Spahn
higher inductive type (Rev #1)

Categorially a higher inductive type is an initial algebra of an endofunctor.

In particular WW-types correspond to initial algebras of polynomial functors.

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

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