1Categorially 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{\array{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{\array{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. (...) ## Extensional $W$-types The rules for $W$-types in extensional type theory are from the notes to Martin-Löf's lecture on intuitionistic type theories. (1) $W$-formation rule $$\frac{A:Type\; x:A\vdash B(x):Type}{(Wx:A)B(x):Type}$$ In the following we will sometimes abbreviate $(Wx:A)B(x)$ by $W$ (2) $W$-introduction rule $$\frac{a:A\; t:B(a)\to W}{sup(a,t):W}$$ (3) $W$-elimination rule $$\frac{\array{w:W\vdash C(w):Type\\ x:A, u:B(x)\to W, v:(\Pi y:B(x))C(u(y))\vdash\\ c(x,y,v):C(sup(x,y))}}{w:W\vdash wrec(w,c):C(w)}$$ (4) $W$-computation rule $$\frac{\array{w:W\vdash C(w):Type\\ x:A, u:B(x)\to W, v:(\Pi y:B(x))C(u(y))\vdash\\ c(x,y,v):C(sup(x,y))}}{\array{ x:A, u:B(x)\to W\vdash wrec(sup(x,u),c)=\\ c(x,u,\lambda y.wrec(u(y),c)):C(sup(x,u))}}$$ Comments: We can think of $W$-types as free algebras for signatures with operations of possibly infinite arity, but no equations: (ad1) We consider the premises of this rule as specifying a signature which has the elements of $A$ as operations and in which the arity of $a:A$ is the cardinality of the type $B(a)$. (ad2) Then, the introduction rule -as always- specifies the canonical way of forming an element of the type in consideration. (ad3) The elimination rule can be interpreted as the propositions-as-types translation of the appropriate induction principle. In more detail, let $\mathcal{H}_ext$ denote the type theory obtained form $\mathcal{H}$ by adopting the identity reflection rule $\frac{p:Id_A(x,y)}{x=y:A}$ and let $\mathcal{C}(\mathcal{H}_ext)$ denote the category types as objects and function types $f:A\to B$ as morphisms where two maps are considered to be equal if they are definitionally equal. Then, the premisses of the introduction rule determine the [[nLab:polynomial functor|polynomial endofunctor]] $P:\mathcal{C}(\mathcal{H}_ext)\to \mathcal{C}(\mathcal{H}_ext)$ defined by $$P(X)=_{def}(\Sigma x: A)(B(x)\to X).$$ A *$P$-algebra* is a pair $(C,s_C)$ where $C$ is a type and $s_C:PC\to C$ is a function called the *structure map of the algebra*. The formation rule gives us an object $W=_{def} (Wx:A)B(x)$. The introduction rule combined with the rule for $\Pi$-types and $\Sigma$-types determines a structure map $s_W:PW\to W$. The elimination rule implies that the projection $\pi_1:C\to W$ where $C=_{def} (\Sigma w:W)C(w)$ has a section if the type $C$ has a $P$-algebra structure over $W$ The computation rule states that the section $s$ determined by the elimination rule is also a $P$-algebra homomorphism. ## 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. * P. Martin-Löf, Intuitionistic Type Theory. Notes by G. Sambin of a series of lectures given in Padua, 1980. Bibliopolis, 1984.