Spahn higher inductive type (Rev #14, changes)

Showing changes from revision #13 to #14: Added | Removed | Changed

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

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

(2) $Id$-introduction rule

(3) $Id$-elimination rule

(4) $Id$-computation rule

One important effect of not having the identity-reflection rule

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

is inhabited.

(5) the Function extensionality axiom (FE): the rule asserting that for every $f,g:A\to B$, the type

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

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

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

In the following we will sometimes abbreviate $(Wx:A)B(x)$ by $W$

(2) $W$-introduction rule

(3) $W$-elimination rule

(4) $W$-computation rule

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]]polynomial endofunctor$P:\mathcal{C}(\mathcal{H}_ext)\to \mathcal{C}(\mathcal{H}_ext)$ $P:\mathcal{C}(\mathcal{H}_ext)\to \mathcal{C}(\mathcal{H}_ext)$ defined by

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$\mathrm{<span><del\; class="diffmod">\; C</del><ins\; class="diffmod">\; s</ins></span>}$ C s has if a the type$\mathrm{<span><del\; class="diffmod">\; P</del><ins\; class="diffmod">\; C</ins></span>}$ P C -algebra structure has over a$\mathrm{<span><del\; class="diffmod">\; W</del><ins\; class="diffmod">\; P</ins></span>}$ W P-algebra structure over $W$

The computation rule states that the section $s$ determined by the elimination rule is also a $P$-algebra homomorphism.

The previous elimination rule implies the simple $W-elimination rule

$$\frac{C:Type\; x:A,v:B(x)\to C\vdash c(x,v):C}{w:W\vdash simp-wrec(w,c):C}$$

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.