Spahn higher inductive type (Rev #1, changes)

Showing changes from revision #0 to #1: Added | ~~Removed~~ | ~~Chan~~ged

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

In particular $W$ -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.