nLab Martin-Löf dependent type theory

Redirected from "intuitionistic 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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

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.

Formal presentation

There are many different ways to present Martin-Löf dependent type theory in a formal system. In this article, we give a formal presentation of Martin-Löf dependent type theory in the framework of natural deduction, one which has a separate type judgment and no type universes.

Judgments and contexts

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 necessarily 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 succesively dependent types. The variables may be defined as de Bruijn indices, in which case the type of a variable nn is given by nnth 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 the basic judgement forms:

  • Γctx\Gamma \; \mathrm{ctx}

    saying that: “Γ\Gamma is a well-formed context”;

  • ΓAtype\Gamma \vdash A\; \mathrm{type}

    saying that “AA is a well-typed dependent type in context Γ\Gamma”;

  • Γa:A\Gamma \vdash a : A

    saying that “aa is a well-typed term of type AA in context Γ\Gamma”;

The following table indicates the corresponding categorical semantics of these notions of dependent type theory:

We work in the logical framework of natural deduction, where everything is given by inference rules.

To start with, contexts are built from dependent types by the following rules (cf. type telescope):

()ctxΓctxΓAtype(Γ,a:A)ctx \frac{}{() \; \mathrm{ctx}} \qquad \frac{\Gamma \; \mathrm{ctx} \quad \Gamma \vdash A \; \mathrm{type}}{(\Gamma, a:A) \; \mathrm{ctx}}

Structural rules

Among the structural rules of dependent type theory are (e.g. Jacobs (1998), p. 122, UFP13, A.2.2, Rijke (2018), Sec. 1.4):

shown in the following table together with their categorical semantics of dependent types:

The weakening and substitution rules are admissible rules: they do not need to be explicitly included in the type theory as they could be proven by induction on the structure of all possible derivations.

Definitional equality

In addition, there are judgments for definitional equality of types and of terms:

  • ΓAAtype\Gamma \vdash A \equiv A' \; \mathrm{type} - AA and AA' are judgementally equal well-typed types in context Γ\Gamma.
  • Γaa:A\Gamma \vdash a \equiv a' : A - aa and aa' are judgementally equal well-typed terms of type AA in context Γ\Gamma.

Definitional equality has its own structural rules: reflexivity, symmetry, transitivity, the principle of substitution, and the variable conversion rule.

  • Reflexivity of definitional equality
ΓAtypeΓAAtype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A \equiv A \; \mathrm{type}}
ΓAtypeΓa:AΓaa:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a \equiv a:A}
  • Symmetry of definitional equality

    ΓABtypeΓBAtype\frac{\Gamma \vdash A \equiv B \; \mathrm{type}}{\Gamma \vdash B \equiv A \; \mathrm{type}}
    ΓAtypeΓab:AΓba:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b:A}{\Gamma \vdash b \equiv a:A}
  • Transitivity of definitional equality

    ΓABtypeΓBCtypeΓACtype\frac{\Gamma \vdash A \equiv B \; \mathrm{type} \quad \Gamma \vdash B \equiv C \; \mathrm{type} }{\Gamma \vdash A \equiv C \; \mathrm{type}}
    ΓAtypeΓab:Abc:AΓac:A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b:A \quad b \equiv c:A }{\Gamma \vdash a \equiv c:A}
  • Principle of substitution of definitionally equal terms:

    ΓAtypeΓab:AΓ,x:A,ΔBtypeΓ,Δ[b/x]B[a/x]B[b/x]type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash B[a/x] \equiv B[b/x] \; \mathrm{type}}
    ΓAtypeΓab:AΓ,x:A,Δc:BΓ,Δ[b/x]c[a/x]c[b/x]:B[b/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a \equiv b : A \quad \Gamma, x:A, \Delta \vdash c:B}{\Gamma, \Delta[b/x] \vdash c[a/x] \equiv c[b/x]: B[b/x]}
  • Variable conversion rule:

    ΓABtypeΓ,x:A,Δ𝒥Γ,x:B,Δ𝒥\frac{\Gamma \vdash A \equiv B \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash \mathcal{J}}{\Gamma, x:B, \Delta \vdash \mathcal{J}}

Definitions

In addition, there are judgments for the initialization operator for types and for terms:

  • ΓAAtype\Gamma \vdash A' \coloneqq A \; \mathrm{type} - AA' is defined to be the type AA in context Γ\Gamma.
  • Γaa:A\Gamma \vdash a' \coloneqq a : A - aa' is defined to be the term a:Aa:A of type AA in context Γ\Gamma.

The initialization operator has its own structural rules: type formation, term introduction, and equality reflection.

  • Formation and judgmental equality reflection rules for type definition:

    ΓBAtypeΓBtypeΓBAtypeΓBAtype\frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash B \; \mathrm{type}} \qquad \frac{\Gamma \vdash B \coloneqq A \; \mathrm{type}}{\Gamma \vdash B \equiv A \; \mathrm{type}}
  • Introduction and judgmental equality reflection rules for term definition:

    Γba:AΓb:AΓba:AΓba:A\frac{\Gamma \vdash b \coloneqq a:A}{\Gamma \vdash b:A} \qquad \frac{\Gamma \vdash b \coloneqq a:A}{\Gamma \vdash b \equiv a:A}

Rules for types

Each type in Martin-Löf dependent type theory comes with a type formation rule, a term introduction rule, a term elimination rule, a computation rule, and an optional uniqueness rule. The elimination rules we give here are not contextual elimination rules, and the conversion rules given here are not contextual conversion rules.

Function types

  • Formation rules for function types:
ΓAtypeΓBtypeΓABtype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \to B \; \mathrm{type}}
  • Introduction rules for function types:
Γ,x:Ab(x):BΓ(xb(x)):AB\frac{\Gamma, x:A \vdash b(x):B}{\Gamma \vdash (x \mapsto b(x)):A \to B}
  • Elimination rules for function types:
Γf:ABΓa:AΓf(a):B\frac{\Gamma \vdash f:A \to B \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B}
  • Computation rules for function types:
Γ,x:Ab(x):BΓa:AΓ(xb(x))(a)b:B\frac{\Gamma, x:A \vdash b(x):B \quad \Gamma \vdash a:A}{\Gamma \vdash (x \mapsto b(x))(a) \equiv b:B}
  • Uniqueness rules for function types:
Γf:ABΓf(xf(x)):AB\frac{\Gamma \vdash f:A \to B}{\Gamma \vdash f \equiv (x \mapsto f(x)):A \to B}

Dependent product types

  • Formation rules for dependent product types:
ΓAtypeΓ,x:AB(x)typeΓ x:AB(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \prod_{x:A} B(x) \; \mathrm{type}}
  • Introduction rules for dependent product types:
Γ,x:Ab(x):B(x)Γλ(x:A).b(x): x:AB(x)\frac{\Gamma, x:A \vdash b(x):B(x)}{\Gamma \vdash \lambda(x:A).b(x):\prod_{x:A} B(x)}
  • Elimination rules for dependent product types:
Γf: x:AB(x)Γa:AΓf(a):B[a/x]\frac{\Gamma \vdash f:\prod_{x:A} B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash f(a):B[a/x]}
  • Computation rules for dependent product types:
Γ,x:Ab(x):B(x)Γa:AΓλ(x:A).b(x)(a)b[a/x]:B[a/x]\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \lambda(x:A).b(x)(a) \equiv b[a/x]:B[a/x]}
  • Uniqueness rules for dependent product types:
Γf: x:AB(x)Γfλ(x).f(x): x:AB(x)\frac{\Gamma \vdash f:\prod_{x:A} B(x)}{\Gamma \vdash f \equiv \lambda(x).f(x):\prod_{x:A} B(x)}

Product types

  • Formation rules for product types:
ΓAtypeΓBtypeΓA×Btype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \times B \; \mathrm{type}}
  • Introduction rules for product types:
Γa:AΓb:BΓ(a,b):A×B\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash (a, b):A \times B}
  • Elimination rules for product types:
Γz:A×BΓπ 1(z):AΓz:A×BΓπ 2(z):B\frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:A \times B}{\Gamma \vdash \pi_2(z):B}
  • Computation rules for product types:
Γa:AΓb:BΓπ 1(a,b)a:AΓa:AΓb:BΓπ 2(a,b)b:B\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \pi_1(a, b) \equiv a:A} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \pi_2(a, b) \equiv b:B}
  • Uniqueness rules for product types:
Γz:A×BΓz(π 1(z),π 2(z)):A×B\frac{\Gamma \vdash z:A \times B}{\Gamma \vdash z \equiv (\pi_1(z), \pi_2(z)):A \times B}

Dependent sum types

  • Formation rules for dependent sum types:
ΓAtypeΓ,x:AB(x)typeΓ x:AB(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \sum_{x:A} B(x) \; \mathrm{type}}
  • Introduction rules for dependent sum types:
Γa:AΓb:B[a/x]Γ(a,b): x:AB(x)\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B[a/x]}{\Gamma \vdash (a, b):\sum_{x:A} B(x)}
  • Elimination rules for dependent sum types:
Γz: x:AB(x)Γπ 1(z):AΓz: x:AB(x)Γπ 2(z):B(π 1(z))\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \pi_1(z):A} \qquad \frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash \pi_2(z):B(\pi_1(z))}
  • Computation rules for dependent sum types:
Γa:AΓb:B[a/x]Γπ 1(a,b)a:AΓa:AΓb:B[a/x]Γπ 2(a,b)b:B(π 1(a,b))\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B[a/x]}{\Gamma \vdash \pi_1(a, b) \equiv a:A} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B[a/x]}{\Gamma \vdash \pi_2(a, b) \equiv b:B(\pi_1(a, b))}
  • Uniqueness rules for dependent sum types:
Γz: x:AB(x)Γz(π 1(z),π 2(z)): x:AB(x)\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash z \equiv (\pi_1(z), \pi_2(z)):\sum_{x:A} B(x)}

Sum types

  • Formation rules for sum types:
ΓAtypeΓBtypeΓA+Btype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A + B \; \mathrm{type}}
  • Introduction rules for sum types:
Γa:AΓinl(a):A+BΓb:BΓinr(b):A+B\frac{\Gamma \vdash a:A}{\Gamma \vdash \mathrm{inl}(a):A + B} \qquad \frac{\Gamma \vdash b:B}{\Gamma \vdash \mathrm{inr}(b):A + B}
  • Elimination rules for sum types:
Γ,z:A+BCtypeΓ,x:Ac(x):C(inl(x))Γ,y:Bd(y):C(inr(y))Γe:A+BΓind A+B C(c(x),d(y),e):C(e)\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash e:A + B}{\Gamma \vdash \mathrm{ind}_{A + B}^C(c(x), d(y), e):C(e)}
  • Computation rules for sum types:
Γ,z:A+BCtypeΓ,x:Ac(x):C(inl(x))Γ,y:Bd(y):C(inr(y))Γa:AΓind A+B C(c(x),d(y),inl(a))c(a):C(inl(a))\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash a:A}{\Gamma \vdash \mathrm{ind}_{A + B}^C(c(x), d(y), \mathrm{inl}(a)) \equiv c(a):C(\mathrm{inl}(a))}
Γ,z:A+BCtypeΓ,x:Ac(x):C(inl(x))Γ,y:Bd(y):C(inr(y))Γb:BΓind A+B C(c(x),d(y),inr(b))d(b):C(inr(b))\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash b:B}{\Gamma \vdash \mathrm{ind}_{A + B}^C(c(x), d(y), \mathrm{inr}(b)) \equiv d(b):C(\mathrm{inr}(b))}
  • Uniqueness rules for sum types:
Γ,z:A+BCtypeΓ,x:Ac(x):C(inl(x))Γ,y:Bd(y):C(inr(y))Γe:A+BΓ,x:A+Bu:CΓ,a:Au(inl(a))c(a):C(inl(a))Γ,b:Bu(inr(b))d(b):C(inr(b))Γu(e)ind A+B C(c(inl(e)),d(inl(e)),e):C(e)\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c(x):C(\mathrm{inl}(x)) \quad \Gamma, y:B \vdash d(y):C(\mathrm{inr}(y)) \quad \Gamma \vdash e:A + B \quad \Gamma, x:A + B \vdash u:C \quad \Gamma, a:A \vdash u(\mathrm{inl}(a)) \equiv c(a):C(\mathrm{inl}(a)) \quad \Gamma, b:B \vdash u(\mathrm{inr}(b)) \equiv d(b):C(\mathrm{inr}(b))}{\Gamma \vdash u(e) \equiv \mathrm{ind}_{A + B}^C(c(\mathrm{inl}(e)), d(\mathrm{inl}(e)), e):C(e)}

Empty type

  • Formation rules for the empty type:
ΓctxΓ𝟘type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{0} \; \mathrm{type}}
  • Elimination rules for the empty type:
Γ,x:𝟘CtypeΓp:𝟘Γind 𝟘 C(p):C(p)\frac{\Gamma, x:\mathbb{0} \vdash C \; \mathrm{type} \quad \Gamma \vdash p:\mathbb{0}}{\Gamma \vdash \mathrm{ind}_\mathbb{0}^C(p):C(p)}
  • Uniqueness rules for the empty type:
Γ,x:𝟘CtypeΓp:𝟘Γ,x:𝟘u:CΓu[p/x]ind 𝟘 C(p):C[p/x]\frac{\Gamma, x:\mathbb{0} \vdash C \; \mathrm{type} \quad \Gamma \vdash p:\mathbb{0} \quad \Gamma, x:\mathbb{0} \vdash u:C}{\Gamma \vdash u[p/x] \equiv \mathrm{ind}_\mathbb{0}^{C}(p):C[p/x]}

Unit type

  • Formation rules for the unit type:
ΓctxΓ𝟙type\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{1} \; \mathrm{type}}
  • Introduction rules for the unit type:
ΓctxΓ*:𝟙\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash *:\mathbb{1}}
  • Elimination rules for the unit type:
Γ,x:𝟙CtypeΓc *:C[*/x]Γp:𝟙Γind 𝟙 C(p,c *):C[p/x]\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x] \quad \Gamma \vdash p:\mathbb{1}}{\Gamma \vdash \mathrm{ind}_\mathbb{1}^C(p, c_*):C[p/x]}
  • Computation rules for the unit type:
Γ,x:𝟙CtypeΓc *:C[*/x]Γind 𝟙 C(*,c *)c *:C[*/x]\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x]}{\Gamma \vdash \mathrm{ind}_\mathbb{1}^C(*, c_*) \equiv c_*:C[*/x]}
  • Uniqueness rules for the unit type:
Γ,x:𝟙CtypeΓc *:C[*/x]Γp:𝟙Γ,x:𝟙u:CΓu[*/x]c *:C[*/x]Γu[p/x]ind 𝟙 C(p,c *):C[p/x]\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x] \quad \Gamma \vdash p:\mathbb{1} \quad \Gamma, x:\mathbb{1} \vdash u:C \quad \Gamma \vdash u[*/x] \equiv c_*:C[*/x]}{\Gamma \vdash u[p/x] \equiv \mathrm{ind}_\mathbb{1}^{C}(p, c_*):C[p/x]}

Natural numbers

  • Formation rules for the natural numbers:

    ΓctxΓtype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N} \; \mathrm{type}}
  • Introduction rules for the natural numbers:

    ΓctxΓ0:Γn:Γs(n):\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{N}} \qquad \frac{\Gamma \vdash n:\mathbb{N}}{\Gamma \vdash s(n):\mathbb{N}}
  • Elimination rules for the natural numbers:

    Γ,x:CtypeΓc 0:C[0/x]Γ,x:,c:Cc s:C[s(x)/x]Γn:Γind C(n,c 0,c s):C[n/x]\frac{\Gamma, x:\mathbb{N} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x] \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C(n, c_0, c_s):C[n/x]}
  • Computation rules for the natural numbers:

    Γ,x:C(x)typeΓc 0:C(0)Γ,x:,c:Cc s:C[s(x)/x]Γind C(0,c 0,c s)c 0:C[0/x]\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x]}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C(0, c_0, c_s) \equiv c_0:C[0/x]}
Γ,x:C(x)typeΓc 0:C(0)Γ,x:,c:Cc s:C[s(x)/x]Γind C(s(n),c 0,c s)c s(n,ind C(n,c 0,c s)):C[s(n)/x]\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x]}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C(s(n), c_0, c_s) \equiv c_s(n, \mathrm{ind}_\mathbb{N}^C(n, c_0, c_s)):C[s(n)/x]}
  • Uniqueness rules for the natural numbers:
    Γ,x:CtypeΓc 0:C[0/x]Γ,x:,c:Cc s:C[s(x)/x]Γn:Γ,x:u:CΓi 0(u):u[0/x]= C[0/x]c 0Γ,x:i s(u):u[s(x)/x]= C[s(x)/x]c s[u/c]Γu[n/x]ind C(p,c 0,c s):C[n/x]\frac{\Gamma, x:\mathbb{N} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_0:C[0/x] \quad \Gamma, x:\mathbb{N}, c:C \vdash c_s:C[s(x)/x] \quad \Gamma \vdash n:\mathbb{N} \quad \Gamma, x:\mathbb{N} \vdash u:C \quad \Gamma \vdash i_0(u):u[0/x] =_{C[0/x]} c_0 \quad \Gamma, x:\mathbb{N} \vdash i_s(u):u[s(x)/x] =_{C[s(x)/x]} c_s[u/c]}{\Gamma \vdash u[n/x] \equiv \mathrm{ind}_\mathbb{N}^{C}(p, c_0, c_s):C[n/x]}

Identity types

There is another version of equality, called the identity type or typal equality, because this equality is a type. The identity type is only be used for equality between terms of a type, and unless one is using Russell universes where types are represented by terms of a Russell universe, identity types cannot be used for equality of types.

  • Formation rule for identity types:
ΓAtypeΓ,a:A,b:Aa= Abtype\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, b:A \vdash a =_A b \; \mathrm{type}}
  • Introduction rule for identity types:
ΓAtypeΓ,a:Arefl A(a):a= Aa\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A \vdash \mathrm{refl}_A(a) : a =_A a}
  • Elimination rule for identity types:

    Γ,a:A,b:A,p:a= AbCtypeΓ,c:At:C[c/a,c/b,refl A(c)/p]Γ,a:A,b:A,p:a= AbJ(t,a,b,p):C\frac{\Gamma, a:A, b:A, p:a =_A b \vdash C \mathrm{type} \quad \Gamma, c:A \vdash t:C[c/a, c/b, \mathrm{refl}_A(c)/p]}{\Gamma, a:A, b:A, p:a =_A b \vdash J(t, a, b, p):C}
  • Computation rules for identity types:

    Γ,a:A,b:A,p:a= AbCtypeΓ,c:At:C[c/a,c/b,refl A(c)/p]Γ,c:AJ(t,c,c,refl(c))t:C[c/a,c/b,refl A(c)/p]\frac{\Gamma, a:A, b:A, p:a =_A b \vdash C \; \mathrm{type} \quad \Gamma, c:A \vdash t:C[c/a, c/b, \mathrm{refl}_A(c)/p]}{\Gamma, c:A \vdash J(t, c, c, \mathrm{refl}(c)) \equiv t:C[c/a, c/b, \mathrm{refl}_A(c)/p]}
  • Optional uniqueness rules for identity types:

Intensional and extensional type theories

In Martin-Löf dependent type theory, one makes a distinction between intensional and extensional type theories. A Martin-Löf dependent type theory is an extensional type theory if there is an equality reflection rule where from typal equality of terms, one could derive definitional equality of terms:

Γ,a:A,b:Ap:a= AbΓ,a:A,b:Aab:A\frac{\Gamma, a:A, b:A \vdash p:a =_A b}{\Gamma, a:A, b:A \vdash a \equiv b:A}

The type theory is an intensional type theory if it doesn’t have the equality reflection rule.

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

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 and at dependent type theory.

The original articles:

As a programming language:

  • Per Martin-Löf, Constructive Mathematics and Computer Programming, in: Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979), Studies in Logic and the Foundations of Mathematics 104 (1982) 153-175 [doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0]

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

Further discussion:

also published as:

Textbook accounts on general dependent type theory:

Martin-Löf type theory is discussed in chapter 7 of:

A philosophical examination:

An introduction and survey (with an eye towards homotopy type theory):

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

as well as

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)

Last revised on May 16, 2025 at 03:50:09. See the history of this page for a list of all contributions to it.