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