Spahn
higher inductive type (Rev #12)

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 WW-types in an extensional type theory correspond to initial algebras of polynomial functors. Also this is not true for intensional type theories.

This failure of intensional type theory can be (at least for WW-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

Extensional vs. intensional type theories

The four standard forms of typing judgements are

(1) A:TypeA:Type

(2) A=B:TypeA=B:Type definitional equality for types

(3) a:Aa:A

(4) a=b:Aa=b:A definitional equality for termes

There is also another notion of equality - namely propositional equality:

Rules for identity types

(1) IdId-formation rule

A:Typea:Ab:AId A(a,b):Type\frac{A:Type\; a:A\; b:A}{Id_A(a,b):Type}

(2) IdId-introduction rule

a:Arefl(a):Id A(a,a)\frac{a:A}{refl(a):Id_A(a,a)}

(3) IdId-elimination rule

a,y:A,u:Id A(x,y)C(x,y,u):Type x:Ac(x):C(x,x,refl(x))x,y:A,u:Id A(x,y)idrec(x,y,u,c):C(x,y,u)\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) IdId-computation rule

a,y:A,u:Id A(x,y)C(x,y,u):Type x:Ac(x):C(x,x,refl(x))x:Aidrec(x,x,refl(x),c)=c(x):C(x,xrefl(x))\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

p:Id A(x,y)x=y:A\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 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,λx,app(f,x),app(g,x))Id AB(f,g)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:ABf,g:A\to B, the type

(Πx:A)Id B(app(f,x),app(g,x)))Id AB(f,g)(\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)p:Id(a,b) is interpreted as a path between the points aa and bb. More generally an identity term p(x):Id(a(x),b(x))p(x):Id(a(x),b(x)) with free variable xx 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:AB(x):Typex:A\vdash B(x):Type

and an identity term p:Id A(a,b)p:Id_A(a,b), there is a transport function

p !:B(a)B(b).p_!:B(a)\to B(b).

For x:Ax:A the function refl(x) !:B(x)B(x)refl(x)_!:B(x)\to B(x) is obtained by IdId-elimination.

(…)

Extensional WW-types

The rules for WW-types in extensional type theory are from the notes to Martin-Löf’s lecture on intuitionistic type theories.

(1) WW-formation rule

A:Typex:AB(x):Type(Wx:A)B(x):Type\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)(Wx:A)B(x) by WW

(2) WW-introduction rule

a:At:B(a)Wsup(a,t):W\frac{a:A\; t:B(a)\to W}{sup(a,t):W}

(3) WW-elimination rule

w:WC(w):Type x:A,u:B(x)W,v:(Πy:B(x))C(u(y)) c(x,y,v):C(sup(x,y))w:Wwrec(w,c):C(w)\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) WW-computation rule

w:WC(w):Type x:A,u:B(x)W,v:(Πy:B(x))C(u(y)) c(x,y,v):C(sup(x,y))x:A,u:B(x)Wwrec(sup(x,u),c)= c(x,u,λy.wrec(u(y),c)):C(sup(x,u))\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 WW-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 AA as operations and in which the arity of a:Aa:A is the cardinality of the type B(a)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 ext\mathcal{H}_ext denote the type theory obtained form \mathcal{H} by adopting the identity reflection rule p:Id A(x,y)x=y:A\frac{p:Id_A(x,y)}{x=y:A} and let 𝒞( ext)\mathcal{C}(\mathcal{H}_ext) denote the category types as objects and function types f:ABf: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 polynomial endofunctor P:𝒞( ext)𝒞( ext)P:\mathcal{C}(\mathcal{H}_ext)\to \mathcal{C}(\mathcal{H}_ext) defined by

P(X)= def(Σx:A)(B(x)X).P(X)=_{def}(\Sigma x: A)(B(x)\to X).

A PP-algebra is a pair (C,s C)(C,s_C) where CC is a type and s C:PCCs_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)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:PWWs_W:PW\to W.

The elimination rule implies that the projection π 1:CW\pi_1:C\to W where C= def(Σw:W)C(w)C=_{def} (\Sigma w:W)C(w) has a section if the type CC has a PP-algebra structure over WW

The computation rule states that the section ss determined by the elimination rule is also a PP-algebra homomorphism.

References

  • Steve Awodey, Nicola gambino, Kristina Sojakova, inductive types in homotopy type theory, arXiv:1201.3898

  • S. Awodey, Type theory and homotopy, 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.

Revision on February 27, 2013 at 00:19:53 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.