nLab Martin-Löf dependent type theory

Idea

Per Martin-Löf‘s dependent type theory, also known as intuitionistic type theory (Martin-Löf 75), 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.

Syntax

The syntax of Martin-Löf dependent type theory can be constructed in two stages. The first is the raw or untyped syntax of the theory consisting of expressions that are readable but not meaningful. The second stage consists of defining the derivable judgements of the type theory inductively which then pick out the meaningful contexts, types and terms.

A context is a list of types. Variables can be defined as De Bruijn indices in which case the type of a variable $n$ is given by $n$th type in a context.

One may also define contexts as coming with a variable name, in which case one needs a notion of $\alpha$-equivalence (syntactic identity modulo renaming of bound variables) and of capture-free substitution. De Bruijn indices avoid this step but can be more obfuscating.

Types and terms are built inductively from various constructors. Types, terms and contexts are defined mutually.

We have four basic judgement forms:

• $\Gamma \vdash A\; \mathrm{type}$ - $A$ is a well-typed type in context $\Gamma$.
• $\Gamma \vdash A \cong A' \; \mathrm{type}$ - $A$ and $A'$ are judgementally equal well-typed types in context $\Gamma$.
• $\Gamma \vdash a : A$ - $a$ is a well-typed term of type $A$ in context $\Gamma$.
• $\Gamma \vdash a \cong a' : A$ - $a$ and $a'$ are judgementally equal well-typed terms of type $A$ in context $\Gamma$.

There is also a fifth judgement that a given context is well-formed. This can be defined from the other judgments as every type in a context is well-typed in the presence of the types that precede it.

Syntax

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:

• The empty list is a valid context.
• If $\Gamma$ is a valid context, $x$ is a variable not appearing in $\Gamma$, and $A$ is a valid type in the context $\Gamma$, then the context obtained by appending $x : A$ to $\Gamma$ is also valid.

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

Binary product types

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

Unit type

There is an atomic type called $\top$.

For any context $\Gamma$ we have $\Gamma \vdash \mathrm{tt} : \top$.

Dependent product types

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

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

Binary sum types

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 \sigma_0 (a) : A + B$; and if $\Gamma \vdash b : B$ and $\Gamma \vdash A + B : \mathrm{Type}$, then $\Gamma \vdash \sigma_1(b) : A + B$.

If $\Gamma \vdash s : A + B$, $\Delta, x : A \vdash c(x) : C(\sigma_0(x))$ and $E, y : B \vdash c'(y) : C(\sigma_1(y))$, then $\Gamma, \Delta, E \vdash \mathrm{cases}(s, (\lambda x : A) c(x), (\lambda y : B) c'(y)) : C(s)$.

Empty type

There is an atomic type called $\bot$.

If $\Gamma \vdash A : \mathrm{Type}$, then $\Gamma, x : \bot \vdash \mathrm{abort} : A$.

Dependent sum types

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

Finite types

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.

Propositions as types

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:

• Conjunction introduction:
  $$\frac{\Gamma \vdash A : \mathrm{true} ; \Delta \vdash B : \mathrm{true}}{\Gamma, \Delta \vdash A \times B : \mathrm{true}}$$
• Conjunction elimination:
  $$\begin{aligned} \frac{\Gamma \vdash A \times B : \mathrm{true}}{\Gamma \vdash A : \mathrm{true}} \,\, & \frac{\Gamma \vdash A \times B : \mathrm{true}}{\Gamma \vdash B : \mathrm{true}} \end{aligned}$$
• Truth introduction
  $$\frac{}{\Gamma \vdash \top : \mathrm{true}}$$
• Universal generalisation:
  $$\frac{\Gamma, x : X \vdash A(x) : \mathrm{true}}{\Gamma \vdash (\Pi x : X) A(x) : \mathrm{true}}$$
• Universal instantiation:
  $$\frac{\Gamma \vdash (\Pi x : X) A(x) : \mathrm{true} ; \Delta \vdash t : X}{\Gamma, \Delta \vdash A(t) : \mathrm{true}}$$
• Conditional proof (implication introduction):
  $$\frac{\Gamma, X : \mathrm{true} \vdash A : \mathrm{true}}{\Gamma \vdash X \to A : \mathrm{true}}$$
• Modus ponens (implication elimination):
  $$\frac{\Gamma \vdash X \to A : \mathrm{true} ; \Delta \vdash X : \mathrm{true}}{\Gamma, \Delta \vdash A : \mathrm{true}}$$
• Disjunction introduction:
  $$\begin{aligned} \frac{\Gamma \vdash A : \mathrm{true}}{\Gamma \vdash A + B : \mathrm{true}} \,\, & \frac{\Gamma \vdash B : \mathrm{true}}{\Gamma \vdash A + B : \mathrm{true}} \end{aligned}$$
• Disjunction elimination:
  $$\frac{\Gamma \vdash A + B : \mathrm{true} ; \Delta, A : \mathrm{true} \vdash C : \mathrm{true} ; E, B : \mathrm{true} \vdash C : \mathrm{true}}{\Gamma, \Delta, E \vdash C : \mathrm{true}}$$
• False elimination:
  $$\frac{\Gamma \vdash \bot : \mathrm{true}}{\Gamma \vdash A : \mathrm{true}}$$
• Existential generalisation:
  $$\frac{\Gamma \vdash t : X ; \Gamma \vdash A(t) : \mathrm{true}}{\Gamma \vdash (\Sigma x : X) A(x) : \mathrm{true}}$$
• Existential instantiation:
  $$\frac{\Gamma \vdash (\Sigma x : X) A(x) : \mathrm{true} ; \Delta, x : X, A(x) : \mathrm{true} \vdash B : \mathrm{true}}{\Gamma, \Delta \vdash B : \mathrm{true}}$$

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.

Equality types

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.

Finite product types

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

Unit type

If $\Gamma \vdash a : \top$, then $\Gamma \vdash a = \mathrm{tt} : \mathrm{true}$.

Dependent product types

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

Function types

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

Binary sum types

If $\Gamma \vdash a : A$ and $\Gamma \vdash A + B : \mathrm{Type}$, $\Delta, x : A \vdash c(x) : C(\sigma_0(x))$ and $E, y : B \vdash c'(y) : C(\sigma_1(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}$

Dependent sum types

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.

Properties

Models and categorical semantics

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.

Axiom of choice

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

Theorem

(ACL)

$$x : A, y : B(x) \vdash C(x, y) : Type \; \vdash \; acl : (\forall x : A) (\exists y : B(x)) C(x, y) \to (\exists f : (\Pi x : A)B(x) )(\forall x : A) C(x, \mathrm{apply}(f, x)) \,.$$

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

Remark

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 ACL then follows since every object of the original category becomes projective in its ex/lex completion.

Remark

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.

Related concepts

• initiality conjecture

type, type theory

• propositions as types, inductive type, W-type

• empty type, unit type

• pointed type

dependent type, dependent type theory, Martin-Löf dependent type theory

• dependent sum type, dependent product type

homotopy type, homotopy type theory

• identity type, dependent identity type

• homotopy n-type, connected type

• higher inductive type

• geometric homotopy type, cohesive homotopy type

References

See also the references at type theory.

The original articles:

• Per Martin-Löf, An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 Pages 73-118, Elsevier 1975 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

• Per Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) (pdf, pdf)

As a programming language:

• Per Martin-Löf, Constructive Mathematics and Computer Programming, Studies in Logic and the Foundations of Mathematics Volume 104, 1982, Pages 153-175 (doi:10.1016/S0049-237X(09)70189-2)

• Bengt Nordström, Kent Petersson, Jan M. Smith, Programming in Martin-Löf’s Type Theory, Oxford University Press 1990 (webpage, pdf)

A philosophical examination:

• Göran Sundholm​, Proof Theory and Meaning (1986), (pdf)

An introduction and survey (with an eye towards homotopy type theory) is in chapter 1 of

• Michael Warren, Homotopy theoretic aspects of constructive type theory, PhD thesis (2008) (pdf)

as well as

• Egbert Rijke, Homotopy type theory (2012) (pdf)

A discussion of ML dependent type theory as the internal language of locally cartesian closed categories is in

• R. A. G. Seely, Locally cartesian closed categories and type theory, Math. Proc. Camb. Phil. Soc. (1984) 95 (pdf)

Discussion of the logical axiom of choice in dependent type theory is in

• John Bell, The Axiom of choice in type theory, Stanford Encyclopedia of philosophy, 2008 (web)

• Tait (1994)