nLab
Martin-Löf dependent type theory

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Foundations

Martin-Löf dependent type theory

Idea

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.

Syntax

If tt is a term, and AA a type, then t:At : A is a typing declaration asserting that tt is a term of type AA. 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, xx is a variable not appearing in Γ\Gamma, and AA is a valid type in the context Γ\Gamma, then the context obtained by appending x:Ax : 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 Γt:A\Gamma \vdash t : A to assert that t:At : A is a valid typing declaration in the context of Γ\Gamma, and by abuse of notation we may write ΓA:Type\Gamma \vdash A : \mathrm{Type} to assert that AA is a valid type in the context of Γ\Gamma.

For any context Γ\Gamma, if AA is an atomic type, ΓA:Type\Gamma \vdash A : \mathrm{Type}.

If x:Ax : A is a typing declaration in Γ\Gamma, then we have Γx:A\Gamma \vdash x : A.

Binary product types

If ΓA:Type\Gamma \vdash A : \mathrm{Type} and ΔB:Type\Delta \vdash B : \mathrm{Type}, then Γ,ΔA×B:Type\Gamma, \Delta \vdash A \times B : \mathrm{Type}.

If Γa:A\Gamma \vdash a : A and Δb:B\Delta \vdash b : B then Γ,Δa,b:A×B\Gamma, \Delta \vdash \langle a, b \rangle : A \times B.

If Γc:A×B\Gamma \vdash c : A \times B, then Γπ 0(c):A\Gamma \vdash \pi_0(c) : A and Γπ 1(c):B\Gamma \vdash \pi_1(c) : B.

Unit type

There is an atomic type called \top.

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

Dependent product types

If Γ,x:XA(x):Type\Gamma, x : X \vdash A(x) : \mathrm{Type}, then Γ(Πx:X)A(x):Type\Gamma \vdash (\Pi x : X) A(x) : \mathrm{Type}.

If Γ,x:Xa(x):A(x)\Gamma, x : X \vdash a(x) : A(x), then Γ(λx:X)a(x):(Πx:X)A(x)\Gamma \vdash (\lambda x : X) a(x) : (\Pi x : X) A(x).

If Γf:(Πx:X)A(x)\Gamma \vdash f : (\Pi x : X) A(x) and Δt:X\Delta \vdash t : X, then Γ,Δapply(f,t):A(t)\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)A(x) does not depend on xx at all. When we write out the rules for dependent products in this case, they become the following.

Firstly, if ΓX:Type\Gamma \vdash X : \mathrm{Type} and ΓA:Type\Gamma \vdash A : \mathrm{Type}, then ΓXA:Type\Gamma \vdash X \to A : \mathrm{Type}.

If Γ,x:Xa(x):A\Gamma, x : X \vdash a(x) : A, then Γ(λx:X)a(x):XA\Gamma \vdash (\lambda x : X) a(x) : X \to A.

If Γf:XA\Gamma \vdash f : X \to A and Δt:X\Delta \vdash t : X, then Γ,Δapply(f,t):A\Gamma, \Delta \vdash \mathrm{apply}(f, t) : A.

Binary sum types

If ΓA:Type\Gamma \vdash A : \mathrm{Type} and ΓB:Type\Gamma \vdash B : \mathrm{Type}, then ΓA+B:Type\Gamma \vdash A + B : \mathrm{Type}.

If Γa:A\Gamma \vdash a : A and ΓA+B:Type\Gamma \vdash A + B : \mathrm{Type}, then Γa:A+B\Gamma \vdash a : A + B; and if Γb:B\Gamma \vdash b : B and ΓA+B:Type\Gamma \vdash A + B : \mathrm{Type}, then Γb:A+B\Gamma \vdash b : A + B.

If Γs:A+B\Gamma \vdash s : A + B, Δ,x:Ac(x):C(x)\Delta, x : A \vdash c(x) : C(x) and E,y:Bc(y):C(y)E, y : B \vdash c'(y) : C(y), then Γ,Δ,Ecases(s,(λx:A)c(x),(λy:B)c(y)):C(s)\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 ΓA:Type\Gamma \vdash A : \mathrm{Type}, then Γ,x:abort:A\Gamma, x : \bot \vdash \mathrm{abort} : A.

Dependent sum types

If Γ,x:XA(x):Type\Gamma, x : X \vdash A(x) : \mathrm{Type}, then Γ(Σx:X)A(x):Type\Gamma \vdash (\Sigma x : X) A(x) : \mathrm{Type}.

If Γt:X\Gamma \vdash t : X, Γa:A(t)\Gamma \vdash a : A(t) and Γ(Σx:X)A(x):Type\Gamma \vdash (\Sigma x : X) A(x) : \mathrm{Type}, then Γ(t,a):(Σx:X)A(x)\Gamma \vdash (t, a) : (\Sigma x : X) A(x).

If Γs:(Σx:X)A(x)\Gamma \vdash s : (\Sigma x : X) A(x) and Δ,x:X,y:A(x)b(x,y):B((x,y))\Delta, x : X, y : A(x) \vdash b(x, y) : B((x, y)), then Γ,Δcases(s,(λx:X)(λy:A(x))b(x,y)):B(s)\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)A(x) does not depend on xx, binary product types (above) can be defined to be dependent sums where A(x)A(x) does not depend on xx.

Finite types

Martin-Löf also includes in his type theory a type n\mathbb{N}_n with exactly nn elements, for every external natural number nn. The types \bot and \top can then be defined as 0\mathbb{N}_0 and 1\mathbb{N}_1, respectively. On the other hand, with \bot and \top given as above, one may define 2=+\mathbb{N}_2 = \top + \top, 3=++\mathbb{N}_3 = \top+\top+\top, and so on (by recursion on the external natural number nn).

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 ΓA:true\Gamma \vdash A : \mathrm{true} for the judgement that AA is inhabited: that is, if Γa:A\Gamma \vdash a : A, then ΓA:true\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:
    ΓA:true;ΔB:trueΓ,ΔA×B:true\frac{\Gamma \vdash A : \mathrm{true} ; \Delta \vdash B : \mathrm{true}}{\Gamma, \Delta \vdash A \times B : \mathrm{true}}
  • Conjunction elimination:
    ΓA×B:trueΓA:true ΓA×B:trueΓB:true\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
    Γ:true\frac{}{\Gamma \vdash \top : \mathrm{true}}
  • Universal generalisation:
    Γ,x:XA(x):trueΓ(Πx:X)A(x):true\frac{\Gamma, x : X \vdash A(x) : \mathrm{true}}{\Gamma \vdash (\Pi x : X) A(x) : \mathrm{true}}
  • Universal instantiation:
    Γ(Πx:X)A(x):true;Δt:XΓ,ΔA(t):true\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):
    Γ,X:trueA:trueΓXA:true\frac{\Gamma, X : \mathrm{true} \vdash A : \mathrm{true}}{\Gamma \vdash X \to A : \mathrm{true}}
  • Modus ponens (implication elimination):
    ΓXA:true;ΔX:trueΓ,ΔA:true\frac{\Gamma \vdash X \to A : \mathrm{true} ; \Delta \vdash X : \mathrm{true}}{\Gamma, \Delta \vdash A : \mathrm{true}}
  • Disjunction introduction:
    ΓA:trueΓA+B:true ΓB:trueΓA+B:true\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:
    ΓA+B:true;Δ,A:trueC:true;E,B:trueC:trueΓ,Δ,EC:true\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:
    Γ:trueΓA:true\frac{\Gamma \vdash \bot : \mathrm{true}}{\Gamma \vdash A : \mathrm{true}}
  • Existential generalisation:
    Γt:X;ΓA(t):trueΓ(Σx:X)A(x):true\frac{\Gamma \vdash t : X ; \Gamma \vdash A(t) : \mathrm{true}}{\Gamma \vdash (\Sigma x : X) A(x) : \mathrm{true}}
  • Existential instantiation:
    Γ(Σx:X)A(x):true;Δ,x:X,A(x):trueB:trueΓ,ΔB:true\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 Γa:A\Gamma \vdash a : A and Δa:A\Delta \vdash a' : A, then Γa=a:Type\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 Γa:A\Gamma \vdash a : A, Γb:A\Gamma \vdash b : A, Γc:A\Gamma \vdash c : A, Γa=b:true\Gamma \vdash a = b : \mathrm{true} and Γb=c:true\Gamma \vdash b = c : \mathrm{true} then Γa=c:true\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 Γa:A\Gamma \vdash a : A, and Γb:B\Gamma \vdash b : B, then Γa=π 0(a,b):true\Gamma \vdash a = \pi_0 (\langle a, b \rangle) : \mathrm{true} and Γπ 1(a,b)=b:true\Gamma \vdash \pi_1 (\langle a, b \rangle) = b : \mathrm{true}.

If Γc:A×B\Gamma \vdash c : A \times B, then c=π 0(c),π 1(c):truec = \langle \pi_0 (c), \pi_1 (c) \rangle : \mathrm{true}.

Unit type

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

Dependent product types

If Γ,x:Xa(x):A(x)\Gamma, x : X \vdash a(x) : A(x) and Δt:X\Delta \vdash t : X, then Γ,Δapply((λx:X)a(x),t)=a(t):true\Gamma, \Delta \vdash \mathrm{apply}((\lambda x : X) a(x), t) = a(t) : \mathrm{true}.

If Γf:(Πx:X)A(x)\Gamma \vdash f : (\Pi x : X) A(x), then Γf=(λx:X)apply(f,x):true\Gamma \vdash f = (\lambda x : X) \mathrm{apply}(f, x) : \mathrm{true}.

Function types

If Γ,x:Xa(x):A\Gamma, x : X \vdash a(x) : A and Δt:X\Delta \vdash t : X, then Γ,Δapply((λx:X)a(x),t)=a(t):true\Gamma, \Delta \vdash \mathrm{apply}((\lambda x : X) a(x), t) = a(t) : \mathrm{true}.

If Γf:XA\Gamma \vdash f : X \to A, then Γf=(λx:X)apply(f,x):true\Gamma \vdash f = (\lambda x : X) \mathrm{apply}(f, x) : \mathrm{true}.

Finite sum types

If Γa:A\Gamma \vdash a : A and ΓA+B:Type\Gamma \vdash A + B : \mathrm{Type}, Δ,x:Ac(x):C(x)\Delta, x : A \vdash c(x) : C(x) and E,y:Bc(y):C(y)E, y : B \vdash c'(y) : C(y), then Γ,Δ,Ecases(a,(λx:A)c(x),(λy:B)c(y))=c(a):true\Gamma, \Delta, E \vdash \mathrm{cases}(a, (\lambda x : A) c(x), (\lambda y : B) c(y)) = c(a) : \mathrm{true} and Γ,Δ,Ecases(b,(λx:A)c(x),(λy:B)c(y))=c(b):true\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 Γt:X\Gamma \vdash t : X, Γa:A(t)\Gamma \vdash a : A(t) and Δ,x:X,y:A(x)b(x,a):B((x,a))\Delta, x : X, y : A(x) \vdash b(x, a) : B((x, a)), then Γ,Δcases((t,a),(λx:X)(λy:A(x))b(x,y))=b(t,a):true\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)C(x,y):Typeacl:(x:A)(y:B(x))C(x,y)(f:(Πx:A)B(x))(x:A)C(x,apply(f,x)). 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 ALC 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.

type, type theory

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

homotopy type, homotopy type theory

References

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)

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)

Revised on September 17, 2013 09:08:37 by Urs Schreiber (89.204.154.108)