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 The four standard forms of typing judgements are (1) $A:Type$ (2) $A=B:Type$ *definitional equality for types* (3) $a:A$ (4) $a=b:A$ *definitional equality for termes* There is also another notion of equality - namely *propositional equality*: ### Rules for identity types (1) $Id$-formation rule $$\frac{A:Type\; a:A\; b:A}{Id_A(a,b):Type}$$ (2) $Id$-introduction rule $$\frac{a:A}{refl(a):Id_A(a,a)}$$ (3) $Id$-elimination rule $$\frac{a,y:A,u:Id_A(x,y)\vdash C(x,y,u):Type\;x:A\vdash c(x):C(x,x,refl(x))}{x,y:A,u:Id_A(x,y)\vdash idrec(x,y,u,c):C(x,y,u)}$$ (4) $Id$-computation rule $$\frac{a,y:A,u:Id_A(x,y)\vdash C(x,y,u):Type\;x:A\vdash c(x):C(x,x,refl(x))}{x:A\vdash idrec(x,x,refl(x),c)=c(x):C(x,xrefl(x))}$$ 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 asserting that for every $f,g:A\to B$, the type $$(\Pi x:A) Id_B(app(f,x),app(g,x)))\to Id_{A\to B}(f,g)$$ Comments: In Voevodsky's Coq files is shown that the $\eta$-rule for dependent functions and the function extensionality principle imply the corresponding function extensionality principle for $\Sigma$-types. is inhabited. The function extensionality axiom (FE) is implied by the univalence axiom. The system $\mathcal{H}$ does not have a global extensionality rule such as the identity reflection rule K or UIP ## Homotopical semantics The *transport function*: An identity term $p:Id(a,b)$ is interpreted as a path between the points $a$ and $b$. More generally an identity term $p(x):Id(a(x),b(x))$ with free variable $x$ is interpreted as a continuous family of paths, i.e. a *homotopy between the continuous functions*. The identity elimination rule implies that type dependency respects identity: For a dependent type $$x:A\vdash B(x):Type$$ and an identity term $p:Id_A(a,b)$, there is a *transport function* $$p_!:B(a)\to B(b).$$ For $x:A$ the function $refl(x)_!:B(x)\to B(x)$ is obtained by $Id$-elimination. ## References * Steve Awodey, Nicola gambino, Kristina Sojakova, inductive types in homotopy type theory, [arXiv:1201.3898](http://arxiv.org/abs/1201.3898) * S. Awodey, Type theory and homotopy, [pdf](http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf) * 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. * V. Voevodsky, Univalent foundations Coq files, 2010, available from the author’s web page.