Spahn higher inductive type (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

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 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

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 assertingthat asserting that for everyf,g:ABf,g:A\to B , the type $Id(f,\lambda

(Π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)

is inhabited.

References

  • Steve Awodey, Nicola gambino, Kristina Sojakova, inductive types in homotopy type theory, arXiv: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.

  • V. Voevodsky, Univalent foundations Coq files, 2010, available from the author’s web page.

Revision on February 26, 2013 at 03:13:14 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.