higher inductive type (Rev #2)

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

This failure can be (at least for WW-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.