natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
= + +
/ | -/ | |
, | ||
of / of | ||
for | for hom-tensor adjunction | |
introduction rule for | for hom-tensor adjunction | |
( of) | ( of) | |
into | into | |
( of) | ( of) | |
, , | ||
higher | ||
/ | -// | |
/ | ||
, () | , | |
(, ) | / | |
(absence of) | (absence of) | |
basic constructions:
:
:
:
strong axioms
further
Per Martin-Löf‘s dependent type theory, also known as intuitionistic type theory, or constructive type theory is a specific form of type theory developed to support constructive mathematics. (Note that both “dependent type theory” and “intuitionistic type theory” may refer more generally to type theories that contain dependent types or are intuitionistic, respectively.)
Martin-Löf’s dependent type theory is notable for several reasons:
One can construct an interpretation of first-order intuitionistic logic by interpreting propositions as types (this is true of most any dependent type theory).
It has a version of a variant of the axiom of choice as a theorem (because of the properties of the above interpretation), see the discussion below.
In its intensional form, it has sufficient computational content to function as a programming language. At the same time, it then has identity types whose presence shows that one is really dealing with a form of homotopy type theory.
If $t$ is a term, and $A$ a type, then $t : A$ is a typing declaration asserting that $t$ is a term of type $A$. We will define the forms of valid terms and types below; to begin with, we assume we have a stock of variables, atomic types, and parametrised types.
A context is a finite ordered list of typing declarations, defined inductively as follows:
Note that this must be considered a mutual inductive definition along with the definition of when a type is valid in a given context, which is to be given below in terms of type constructors.
We write $\Gamma \vdash t : A$ to assert that $t : A$ is a valid typing declaration in the context of $\Gamma$, and by abuse of notation we may write $\Gamma \vdash A : \mathrm{Type}$ to assert that $A$ is a valid type in the context of $\Gamma$.
For any context $\Gamma$, if $A$ is an atomic type, $\Gamma \vdash A : \mathrm{Type}$.
If $x : A$ is a typing declaration in $\Gamma$, then we have $\Gamma \vdash x : A$.
If $\Gamma \vdash A : \mathrm{Type}$ and $\Delta \vdash B : \mathrm{Type}$, then $\Gamma, \Delta \vdash A \times B : \mathrm{Type}$.
If $\Gamma \vdash a : A$ and $\Delta \vdash b : B$ then $\Gamma, \Delta \vdash \langle a, b \rangle : A \times B$.
If $\Gamma \vdash c : A \times B$, then $\Gamma \vdash \pi_0(c) : A$ and $\Gamma \vdash \pi_1(c) : B$.
There is an atomic type called $\top$.
For any context $\Gamma$ we have $\Gamma \vdash \mathrm{tt} : \top$.
If $\Gamma, x : X \vdash A(x) : \mathrm{Type}$, then $\Gamma \vdash (\Pi x : X) A(x) : \mathrm{Type}$.
If $\Gamma, x : X \vdash a(x) : A(x)$, then $\Gamma \vdash (\lambda x : X) a(x) : (\Pi x : X) A(x)$.
If $\Gamma \vdash f : (\Pi x : X) A(x)$ and $\Delta \vdash t : X$, then $\Gamma, \Delta \vdash \mathrm{apply}(f, t) : A(t)$.
Function types may be regarded as a special case of dependent product types, where $A(x)$ does not depend on $x$ at all. When we write out the rules for dependent products in this case, they become the following.
Firstly, if $\Gamma \vdash X : \mathrm{Type}$ and $\Gamma \vdash A : \mathrm{Type}$, then $\Gamma \vdash X \to A : \mathrm{Type}$.
If $\Gamma, x : X \vdash a(x) : A$, then $\Gamma \vdash (\lambda x : X) a(x) : X \to A$.
If $\Gamma \vdash f : X \to A$ and $\Delta \vdash t : X$, then $\Gamma, \Delta \vdash \mathrm{apply}(f, t) : A$.
If $\Gamma \vdash A : \mathrm{Type}$ and $\Gamma \vdash B : \mathrm{Type}$, then $\Gamma \vdash A + B : \mathrm{Type}$.
If $\Gamma \vdash a : A$ and $\Gamma \vdash A + B : \mathrm{Type}$, then $\Gamma \vdash a : A + B$; and if $\Gamma \vdash b : B$ and $\Gamma \vdash A + B : \mathrm{Type}$, then $\Gamma \vdash b : A + B$.
If $\Gamma \vdash s : A + B$, $\Delta, x : A \vdash c(x) : C(x)$ and $E, y : B \vdash c'(y) : C(y)$, then $\Gamma, \Delta, E \vdash \mathrm{cases}(s, (\lambda x : A) c(x), (\lambda y : B) c'(y)) : C(s)$.
There is an atomic type called $\bot$.
If $\Gamma \vdash A : \mathrm{Type}$, then $\Gamma, x : \bot \vdash \mathrm{abort} : A$.
If $\Gamma, x : X \vdash A(x) : \mathrm{Type}$, then $\Gamma \vdash (\Sigma x : X) A(x) : \mathrm{Type}$.
If $\Gamma \vdash t : X$, $\Gamma \vdash a : A(t)$ and $\Gamma \vdash (\Sigma x : X) A(x) : \mathrm{Type}$, then $\Gamma \vdash (t, a) : (\Sigma x : X) A(x)$.
If $\Gamma \vdash s : (\Sigma x : X) A(x)$ and $\Delta, x : X, y : A(x) \vdash b(x, y) : B((x, y))$, then $\Gamma, \Delta \vdash \mathrm{cases}(s, (\lambda x : X)(\lambda y : A(x)) b(x, y)) : B(s)$.
Note that just as function types can be defined to be dependent products where $A(x)$ does not depend on $x$, binary product types (above) can be defined to be dependent sums where $A(x)$ does not depend on $x$.
Martin-Löf also includes in his type theory a type $\mathbb{N}_n$ with exactly $n$ elements, for every external natural number $n$. The types $\bot$ and $\top$ can then be defined as $\mathbb{N}_0$ and $\mathbb{N}_1$, respectively. On the other hand, with $\bot$ and $\top$ given as above, one may define $\mathbb{N}_2 = \top + \top$, $\mathbb{N}_3 = \top+\top+\top$, and so on (by recursion on the external natural number $n$).
Note that we have not included any axiom of infinity, however.
Under the Curry-Howard isomorphism, we may identify propositions with certain atomic types and predicates with certain parametrised types.
An inhabitant of such a proposition-as-a-type is interpreted as a ‘proof’ of that proposition.
We write $\Gamma \vdash A : \mathrm{true}$ for the judgement that $A$ is inhabited: that is, if $\Gamma \vdash a : A$, then $\Gamma \vdash A : \mathrm{true}$. The type-formation rules above are then seen to be the rules of inference for (a fragment of) intuitionistic first-order logic. Indeed, we have:
The only traditional rule of inference we are missing is the rule of excluded middle, so this logic is intuitionistic.
The above interpretation justifies the use of the symbols $\forall$, $\exists$, $\wedge$, $\vee$ instead of $\Pi$, $\Sigma$, $\times$, $+$, when we are using types to represent propositions.
We may introduce a family of equality types for each type and each pair of terms of that type: if $\Gamma \vdash a : A$ and $\Delta \vdash a' : A$, then $\Gamma \vdash a = a' : \mathrm{Type}$.
These are not the intensional identity types which Martin-Löf later introduced as a particular sort of inductive family of types, but instead an extensional notion of equality defined by induction over the class of all types (regarded as inductively defined by the above type-formation clauses). Note that it is essential, for a purpose such as this, that the type-formation clauses be regarded as an inductive definition, rather than as “operations” defined on some pre-existing collection of types: in order to define equality in the way we are about to do, we have to be able to inspect a given type and decide uniquely which rule was used to construct it.
The equality type is reflexive, symmetric, and transitive. That means, for example, if $\Gamma \vdash a : A$, $\Gamma \vdash b : A$, $\Gamma \vdash c : A$, $\Gamma \vdash a = b : \mathrm{true}$ and $\Gamma \vdash b = c : \mathrm{true}$ then $\Gamma \vdash a = c : \mathrm{true}$.
Mike Shulman: Is that (reflexivity, symmetry, and transitivity) a rule we are giving, or an assertion we are making about derivability? I’m a little unsure because the presentation here is slightly different from that in the reference: there Martin-Löf uses both a propositional equality and a judgmental one.
If $\Gamma \vdash a : A$, and $\Gamma \vdash b : B$, then $\Gamma \vdash a = \pi_0 (\langle a, b \rangle) : \mathrm{true}$ and $\Gamma \vdash \pi_1 (\langle a, b \rangle) = b : \mathrm{true}$.
If $\Gamma \vdash c : A \times B$, then $c = \langle \pi_0 (c), \pi_1 (c) \rangle : \mathrm{true}$.
If $\Gamma \vdash a : \top$, then $\Gamma \vdash a = \mathrm{tt} : \mathrm{true}$.
If $\Gamma, x : X \vdash a(x) : A(x)$ and $\Delta \vdash t : X$, then $\Gamma, \Delta \vdash \mathrm{apply}((\lambda x : X) a(x), t) = a(t) : \mathrm{true}$.
If $\Gamma \vdash f : (\Pi x : X) A(x)$, then $\Gamma \vdash f = (\lambda x : X) \mathrm{apply}(f, x) : \mathrm{true}$.
If $\Gamma, x : X \vdash a(x) : A$ and $\Delta \vdash t : X$, then $\Gamma, \Delta \vdash \mathrm{apply}((\lambda x : X) a(x), t) = a(t) : \mathrm{true}$.
If $\Gamma \vdash f : X \to A$, then $\Gamma \vdash f = (\lambda x : X) \mathrm{apply}(f, x) : \mathrm{true}$.
If $\Gamma \vdash a : A$ and $\Gamma \vdash A + B : \mathrm{Type}$, $\Delta, x : A \vdash c(x) : C(x)$ and $E, y : B \vdash c'(y) : C(y)$, then $\Gamma, \Delta, E \vdash \mathrm{cases}(a, (\lambda x : A) c(x), (\lambda y : B) c(y)) = c(a) : \mathrm{true}$ and $\Gamma, \Delta, E \vdash \mathrm{cases}(b, (\lambda x : A) c(x), (\lambda y : B) c'(y)) = c'(b) : \mathrm{true}$
If $\Gamma \vdash t : X$, $\Gamma \vdash a : A(t)$ and $\Delta, x : X, y : A(x) \vdash b(x, a) : B((x, a))$, then $\Gamma, \Delta \vdash \mathrm{cases}((t, a), (\lambda x : X)(\lambda y : A(x)) b(x, y)) = b(t, a) : \mathrm{true}$.
The other equality rule for dependent sum types is derivable from the above.
The models of ML type theory depend crucially on whether one considers the variant of extensional type theory or that of intensional type theory.
The models of the extensional version are (just) locally cartesian closed categories.
The faithful models of the intensional version with identity types are however certain (∞,1)-categories, notably (∞,1)-toposes, presented by simplicial model categories (Warren). For this reason one speaks of homotopy type theory.
For a more detailed discussion of these matters see at relation between type theory and category theory.
In dependent type theory we can verify the following “logical form of the axiom of choice” (Bell, Tait), see also (Rijke, section 2.5.1).
(ACL)
One should note carefully that this “is” only “the axiom of choice” under the above propositions-as-types interpretation of the quantifiers $\forall$ and $\exists$.
In the categorical semantics of this expression, using the propositions-as-types logic corresponds roughly to working with the subobject lattices in the ex/lex completion of a locally cartesian closed category; the ALC then follows since every object of the original category becomes projective in its ex/lex completion.
If we use instead a different logic over the same type theory, such as bracket types to model the actual subobject lattices in an arbitrary lccc (not necessarily the ex/lex completion of anything), or the hProp logic in homotopy type theory, then the ACL in that logic will not be derivable.
dependent type, dependent type theory, Martin-Löf dependent type theory
homotopy type, homotopy type theory
See also the references at type theory.
The original reference is
Per Martin-Löf, Intuitionistic type theory (1984)
Per Martin-Löf, An intuitionistic theory of types: predicative part, In Logic Colloquium (1973), ed. H. E. Rose and J. C. Shepherdson (North-Holland, 1974), 73-118. (web)
A philosophical examination is
An introduction and survey (with an eye towards homotopy type theory) is in chapter 1 of
as well as
A discussion of ML dependent type theory as the internal language of locally cartesian closed categories is in
Discussion of the logical axiom of choice in dependent type theory is in
Last revised on June 7, 2018 at 03:26:01. See the history of this page for a list of all contributions to it.