Spahn higher inductive type (Rev #1)

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