Spahn higher inductive type (Rev #3)

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$-types in an extensional type theory correspond to initial algebras of polynomial functors. Also this is not true for intensional type theories.

This failure of intensional type theory 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

Extensional vs. intensional type theories

One important effect of not having the identity-reflection rule

is that it is impossible to prove that the empty type is an initial object.