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