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 of intensional type theory 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) ## Extensional vs. intensional type theories One important effect of not having the *identity-reflection rule* $$\frac{p:Id_A(x,y)}{x=y:A}$$ is that it is impossible to prove that the empty type is an initial object. There are some *extensionality principles* which are weaker than the identity reflection rule: Streicher's K-rule, the *Uniqueness of Identity Proofs* (UIP) which also has benn considered in context of Observational Type Theory. However these constructions seem to be ad hoc and lack a conceptual basis. ## The system $\mathcal{H}$ The dependent type theory $\mathcal{H}$ is defined to have -in addition to the [[rules of type theories|standard structural rules]]- the folowing rules: (1) the rules for identity types. (2) rules for $\Sigma$-types as presented in Nordstrom-Petterson-Smith §5.8 (3) rules for $\Pi$-types as presented in Garner §3.2 (4) the propositional $\eta$-rule for $\Pi$-types: the rule asserting that for every $f:(\Pi x:A)B(x), the type $$Id(f,\lambda x,app(f,x),app(g,x))\to Id_{A\to B}(f,g)$$ is inhabited. (5) the Function extensionality axiom (FE): the rule assertingthat for every $f,g:A\to B$, the type $Id(f,\lambda ## References * Steve Awodey, Nicola gambino, Kristina Sojakova, inductive types in homotopy type theory, [arXiv:1201.3898](http://arxiv.org/abs/1201.3898) * T. Streicher, Investigations into intensional type theory, 1993, Habilitation Thesis. Available from the author’s web page. * B. Nordstrom, K. Petersson, and J. Smith, _Martin-Löf type theory_ in Handbook of Logic in Computer Science. Oxford Uni- versity Press, 2000, vol. 5, pp. 1–37 * R. Garner, On the strength of dependent products in the type theory of Martin-Löf, Annals of Pure and Applied Logic, vol. 160, pp. 1–12, 2009.