Spahn higher inductive type (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Categorially a higher inductive type in an extensional type theory is an initial algebra of an endofunctor. In intensional type theory this analogy fails.

In particular $W$ -type s in an extensional type theory correspond to initial algebras ofpolynomial functor s. Also this is not true for intensional type theories.

This failure can be (at least for $W$ -types and some more general cases) remedied by replacing “initial” by “homotopy initial”. This is the main result (to be found in §2) of

Steve Awodey, Nicola gambino, Kristina Sojakova, inductive types in homotopy type theory, arXiv:1201.3898

Revision on February 25, 2013 at 20:44:37 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.