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

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