Spahn higher inductive type (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

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