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 $W$[[W-type|-type]]s in an extensional type theory correspond to initial algebras of [[nLab:polynomial functor]]s. Also this is not true for intensional type theories. This failure can be (at least for $W$-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](http://arxiv.org/abs/1201.3898)