Showing changes from revision #12 to #13:
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
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:
(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 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
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.
(…)
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 polynomial endofunctor $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 $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.
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.