nLab Martin-Löf dependent type theory

Redirected from "Martin-Löf's 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

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 presentations

There are many different ways to present Martin-Löf dependent type theory in a formal system. In this article, we give two formal presentations of Martin-Löf dependent type theory in the framework of natural deduction, one which has judgmental equality and only one level, and another which has a very weak logic over the dependent type theory as well as propositional equality.

Presentation 1

This first presentation uses judgmental equality, and could be contrasted with the second presentation, which uses propositional equality and a very weak logic over dependent type theory.

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.

Presentation 2

This presentation of Martin-Löf dependent type theory uses a very weak logic over dependent type theory, in the sense that while it does have a notion of proposition, predicate, and truth, there are no conjunctions, disjunctions, implications, universal quantifiers, or existential quantifiers in the logic. Here, propositional equality plays the role of definitional equality and computational equality that judgmental equality played in the first presentation.

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

  • ΓAtype\Gamma \vdash A\; \mathrm{type} - AA is a well-typed type in context Γ\Gamma.
  • Γa:A\Gamma \vdash a : A - aa is a well-typed term of type AA in context Γ\Gamma.
  • Γϕprop\Gamma \vdash \phi \; \mathrm{prop} - ϕ\phi is a well-formed proposition in context Γ\Gamma
  • Γϕtrue\Gamma \vdash \phi \; \mathrm{true} - ϕ\phi is a well-formed true proposition in context Γ\Gamma
  • Γctx\Gamma \; \mathrm{ctx} - Γ\Gamma is a well-formed context.

Contexts are defined by the following rules:

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

Structural rules

There are three structural rules in dependent type theory, the variable rule, the weakening rule, and the substitution rule.

The variable rule states that we may derive a typing judgment if the typing judgment is in the context already:

Γ,a:A,ΔctxΓ,a:A,Δa:A\frac{\Gamma, a:A, \Delta \; \mathrm{ctx}}{\Gamma, a:A, \Delta \vdash a:A}

Let 𝒥\mathcal{J} be any arbitrary judgment. Then we have the following rules:

The weakening rule:

Γ,Δ𝒥ΓAtypeΓ,a:A,Δ𝒥\frac{\Gamma, \Delta \vdash \mathcal{J} \quad \Gamma \vdash A \; \mathrm{type}}{\Gamma, a:A, \Delta \vdash \mathcal{J}}

The substitution rule:

Γa:AΓ,b:A,Δ𝒥Γ,Δ[a/b]𝒥[a/b]\frac{\Gamma \vdash a:A \quad \Gamma, b:A, \Delta \vdash \mathcal{J}}{\Gamma, \Delta[a/b] \vdash \mathcal{J}[a/b]}

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

Definitional equality of types and terms is formed by the following rules:

ΓAtypeΓBtypeΓABprop\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash A \equiv B \; \mathrm{prop}}
ΓAtypeΓa:AΓb:AΓa Abprop\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A}{\Gamma \vdash a \equiv_A b \; \mathrm{prop}}

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

  • Reflexivity of definitional equality
ΓAtypeΓAAtrue\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash A \equiv A \; \mathrm{true}}
ΓAtypeΓa:AΓa Aatrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash a \equiv_A a \; \mathrm{true}}
  • Symmetry of definitional equality
ΓAtypeΓBtypeΓABtrueΓBAtrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A \equiv B \; \mathrm{true}}{\Gamma \vdash B \equiv A \; \mathrm{true}}
ΓAtypeΓa:AΓb:AΓa AbtrueΓb Aatrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash a \equiv_A b \; \mathrm{true}}{\Gamma \vdash b \equiv_A a \; \mathrm{true}}
  • Transitivity of definitional equality
ΓAtypeΓBtypeΓCtypeΓABtrueΓBCtrueΓACtrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash A \equiv B \; \mathrm{true} \quad \Gamma \vdash B \equiv C \; \mathrm{true}}{\Gamma \vdash A \equiv C \; \mathrm{true}}
ΓAtypeΓa:AΓb:AΓc:AΓa AbtrueΓb ActrueΓa Actrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash c:A \quad \Gamma \vdash a \equiv_A b \; \mathrm{true} \quad \Gamma \vdash b \equiv_A c \; \mathrm{true}}{\Gamma \vdash a \equiv_A c \; \mathrm{true}}
  • Principle of substitution of definitionally equal terms:

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

ΓAtypeΓBtypeΓABtrueΓ,x:A,Δ𝒥Γ,x:B,Δ𝒥\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash A \equiv B \; \mathrm{true} \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ΓBAtrue\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{true}}
  • Introduction and judgmental equality reflection rules for term definition:

    Γba:AΓb:AΓba:AΓb Aatrue\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 \; \mathrm{true}}

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) Bbtrue\frac{\Gamma, x:A \vdash b(x):B \quad \Gamma \vdash a:A}{\Gamma \vdash (x \mapsto b(x))(a) \equiv_{B} b \; \mathrm{true}}
  • Uniqueness rules for function types:
Γf:ABΓf AB(xf(x))true\frac{\Gamma \vdash f:A \to B}{\Gamma \vdash f \equiv_{A \to B} (x \mapsto f(x)) \; \mathrm{true}}

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]true\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] \; \mathrm{true}}
  • Uniqueness rules for dependent product types:
Γf: x:AB(x)Γf x:AB(x)λ(x).f(x)true\frac{\Gamma \vdash f:\prod_{x:A} B(x)}{\Gamma \vdash f \equiv_{\prod_{x:A} B(x)} \lambda(x).f(x) \; \mathrm{true}}

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) AatrueΓa:AΓb:BΓπ 2(a,b) Bbtrue\frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \pi_1(a, b) \equiv_A a \; \mathrm{true}} \qquad \frac{\Gamma \vdash a:A \quad \Gamma \vdash b:B}{\Gamma \vdash \pi_2(a, b) \equiv_B b \; \mathrm{true}}
  • Uniqueness rules for product types:
Γz:A×BΓz A×B(π 1(z),π 2(z))true\frac{\Gamma \vdash z:A \times B}{\Gamma \vdash z \equiv_{A \times B} (\pi_1(z), \pi_2(z)) \; \mathrm{true}}

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:
Γ,x:Ab(x):B(x)Γa:AΓb:B[a/x]Γ(a,b): x:AB(x)\frac{\Gamma, x:A \vdash b(x):B(x) \quad \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:
Γ,x:Ab(x):B(x)Γa:AΓπ 1(a,b) AatrueΓ,x:Ab:BΓa:AΓπ 2(a,b) B(π 1(a,b))btrue\frac{\Gamma, x:A \vdash b(x):B(x) \quad \Gamma \vdash a:A}{\Gamma \vdash \pi_1(a, b) \equiv_A a \; \mathrm{true}} \qquad \frac{\Gamma, x:A \vdash b:B \quad \Gamma \vdash a:A}{\Gamma \vdash \pi_2(a, b) \equiv_{B(\pi_1(a, b))} b \; \mathrm{true}}
  • Uniqueness rules for dependent sum types:
Γz: x:AB(x)Γz x:AB(x)(π 1(z),π 2(z))true\frac{\Gamma \vdash z:\sum_{x:A} B(x)}{\Gamma \vdash z \equiv_{\sum_{x:A} B(x)} (\pi_1(z), \pi_2(z)) \; \mathrm{true}}

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:C[inl(x)/z]Γ,y:Bd:C[inr(y)/z]Γe:A+BΓind A+B(z.C,c,d,e):C[e/z]\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c:C[\mathrm{inl}(x)/z] \quad \Gamma, y:B \vdash d:C[\mathrm{inr}(y)/z] \quad \Gamma \vdash e:A + B}{\Gamma \vdash \mathrm{ind}_{A + B}(z.C, c, d, e):C[e/z]}
  • Computation rules for sum types:
Γ,z:A+BCtypeΓ,x:Ac:C[inl(x)/z]Γ,y:Bd:C[inr(y)/z]Γa:AΓind A+B(z.C,c,d,inl(a)) C[inl(a)/z]c[a/x]true\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c:C[\mathrm{inl}(x)/z] \quad \Gamma, y:B \vdash d:C[\mathrm{inr}(y)/z] \quad \Gamma \vdash a:A}{\Gamma \vdash \mathrm{ind}_{A + B}(z.C, c, d, \mathrm{inl}(a)) \equiv_{C[\mathrm{inl}(a)/z]} c[a/x] \; \mathrm{true}}
Γ,z:A+BCtypeΓ,x:Ac:C[inl(x)/z]Γ,y:Bd:C[inr(y)/z]Γb:BΓind A+B(z.C,c,d,inr(b)) C[inr(b)/z]d[b/y]true\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c:C[\mathrm{inl}(x)/z] \quad \Gamma, y:B \vdash d:C[\mathrm{inr}(y)/z] \quad \Gamma \vdash b:B}{\Gamma \vdash \mathrm{ind}_{A + B}(z.C, c, d, \mathrm{inr}(b)) \equiv_{C[\mathrm{inr}(b)/z]} d[b/y] \; \mathrm{true}}
  • Uniqueness rules for sum types:
Γ,z:A+BCtypeΓ,x:Ac:C[inl(x)/z]Γ,y:Bd:C[inr(y)/z]Γe:A+BΓ,z:A+Bu:CΓ,a:Au[inl(a)/z] C[inl(a)/z]c[a/x]trueΓ,b:Bu[inr(b)/z] C[inr(b)/z]d[b/y]trueΓu[e/z] C[e/z]ind A+B(z.C,c[inl(e)/x],d[inr(e)/y],e)true\frac{\Gamma, z:A + B \vdash C \; \mathrm{type} \quad \Gamma, x:A \vdash c:C[\mathrm{inl}(x)/z] \quad \Gamma, y:B \vdash d:C[\mathrm{inr}(y)/z] \quad \Gamma \vdash e:A + B \quad \Gamma, z:A + B \vdash u:C \quad \Gamma, a:A \vdash u[\mathrm{inl}(a)/z] \equiv_{C[\mathrm{inl}(a)/z]} c[a/x] \; \mathrm{true} \quad \Gamma, b:B \vdash u[\mathrm{inr}(b)/z] \equiv_{C[\mathrm{inr}(b)/z]} d[b/y] \; \mathrm{true}}{\Gamma \vdash u[e/z] \equiv_{C[e/z]} \mathrm{ind}_{A + B}(z.C, c[\mathrm{inl}(e)/x], d[\mathrm{inr}(e)/y], e) \; \mathrm{true}}

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 𝟘(x.C,p):C[p/x]\frac{\Gamma, x:\mathbb{0} \vdash C \; \mathrm{type} \quad \Gamma \vdash p:\mathbb{0}}{\Gamma \vdash \mathrm{ind}_\mathbb{0}(x.C, p):C[p/x]}
  • Uniqueness rules for the empty type:
Γ,x:𝟘CtypeΓp:𝟘Γ,x:𝟘u:CΓu[p/x] C[p/x]ind 𝟘(x.C,p)true\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_{C[p/x]} \mathrm{ind}_\mathbb{0}(x.C, p) \; \mathrm{true}}

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 𝟙(x.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}(x.C, p, c_*):C[p/x]}
  • Computation rules for the unit type:
Γ,x:𝟙CtypeΓc *:C[*/x]Γind 𝟙(x.C,*,c *) C[*/x]c *true\frac{\Gamma, x:\mathbb{1} \vdash C \; \mathrm{type} \quad \Gamma \vdash c_*:C[*/x]}{\Gamma \vdash \mathrm{ind}_\mathbb{1}(x.C, *, c_*) \equiv_{C[*/x]} c_* \; \mathrm{true}}
  • Uniqueness rules for the unit type:
Γ,x:𝟙CtypeΓc *:C[*/x]Γp:𝟙Γ,x:𝟙u:CΓu[*/x] C[*/x]c *trueΓu[p/x] C[p/x]ind 𝟙(x.C,p,c *)true\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[*/x]} c_* \; \mathrm{true}}{\Gamma \vdash u[p/x] \equiv_{C[p/x]} \mathrm{ind}_\mathbb{1}(x.C, p, c_*) \; \mathrm{true}}

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/x]c 0true\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/x]} c_0 \; \mathrm{true}}
Γ,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)/x]c s(n,ind C(n,c 0,c s))true\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)/x]} c_s(n, \mathrm{ind}_\mathbb{N}^C(n, c_0, c_s)) \; \mathrm{true}}
  • 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]= C[n/x]ind C(p,c 0,c s)true\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] =_{C[n/x]} \mathrm{ind}_\mathbb{N}^{C}(p, c_0, c_s) \; \mathrm{true}}

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)) C[c/a,c/b,refl A(c)/p]ttrue\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_{C[c/a, c/b, \mathrm{refl}_A(c)/p]} t \; \mathrm{true}}
  • 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:Aa Abtrue\frac{\Gamma, a:A, b:A \vdash p:a =_A b}{\Gamma, a:A, b:A \vdash a \equiv_A b \; \mathrm{true}}

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

Propositional reflection and predicate logic

One could add an additional set of rules in this second presentation of Martin-Löf dependent type theory which isn’t available in the first presentation: propositional reflections. Unlike the first presentation, in this presentation, there are two notions of propositions: the external propositions and the internal propositions. The external propositions are the judgmental propositions in the logic layer of Martin-Löf dependent type theory, and correspond to the external logic. On the other hand, the internal propositions are types equipped with a witness of the isProp modality and correspond to the internal logic. They are also called subsingletons or h-propositions. We could make the internal logic imply the external logic with the following proposition reflection rules:

ΓAtypeΓp:isProp(A)Γϕ ApropΓAtypeΓp:isProp(A)Γa:AΓϕ Atrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \phi_A \; \mathrm{prop}} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash a:A}{\Gamma \vdash \phi_A \; \mathrm{true}}

and similar rules for predicates:

Γ,x:A,ΔBtypeΓ,x:A,Δp:isProp(B)Γ,x:A,Δϕ BpropΓ,x:A,ΔBtypeΓ,x:A,Δp:isProp(B)Γ,x:A,Δb:BΓ,x:A,Δϕ Btrue\frac{\Gamma, x:A, \Delta \vdash B \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash p:\mathrm{isProp}(B)}{\Gamma, x:A, \Delta \vdash \phi_B \; \mathrm{prop}} \qquad \frac{\Gamma, x:A, \Delta \vdash B \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash p:\mathrm{isProp}(B) \quad \Gamma, x:A, \Delta \vdash b:B}{\Gamma, x:A, \Delta \vdash \phi_B \; \mathrm{true}}

If the identity types of Martin-Löf dependent type theory have a uniqueness rule such as the K rule or uniqueness of identity proofs, then propositional reflection implies that the type theory is an extensional type theory.

In addition, since the product type and function type preserve types being a subsingleton, the dependent product of a subsingleton-valued type family, and the unit type and empty type are always subsingletons, one could also add the following propositional reflection rules to the theory, defining conjunction, implication, true, false, and bounded universal quantification:

ΓA×BtypeΓp:isProp(A)Γq:isProp(B)Γϕ Aϕ Bprop\frac{\Gamma \vdash A \times B \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:\mathrm{isProp}(B)}{\Gamma \vdash \phi_A \wedge \phi_B \; \mathrm{prop}}
ΓABtypeΓp:isProp(A)Γq:isProp(B)Γϕ Aϕ Bprop\frac{\Gamma \vdash A \to B \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:\mathrm{isProp}(B)}{\Gamma \vdash \phi_A \implies \phi_B \; \mathrm{prop}}
Γ𝟘typeΓpropΓ𝟙typeΓprop\frac{\Gamma \vdash \mathbb{0} \; \mathrm{type}}{\Gamma \vdash \bot \; \mathrm{prop}} \qquad \frac{\Gamma \vdash \mathbb{1} \; \mathrm{type}}{\Gamma \vdash \top \; \mathrm{prop}}
Γ,Δ x:AB(x)typeΓ,x:A,Δq:isProp(B(x))Γ,Δx:A.ϕ B(x)prop\frac{\Gamma, \Delta \vdash \prod_{x:A} B(x) \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash q:\mathrm{isProp}(B(x))}{\Gamma, \Delta \vdash \forall x:A.\phi_B(x) \; \mathrm{prop}}

Adding propositional truncations to Martin-Löf dependent type theory allows for the full intuitionistic logic to be defined, as disjunctions could be defined from the propositional truncation of the sum type, and the existential quantifier could be defined from the propositional truncation of the dependent sum type:

Γ[A+B]typeΓp:isProp(A)Γq:isProp(B)Γϕ Aϕ Bprop\frac{\Gamma \vdash [A + B] \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma\vdash q:\mathrm{isProp}(B)}{\Gamma \vdash \phi_A \vee \phi_B \; \mathrm{prop}}
Γ,Δ[ x:AB(x)]typeΓ,x:A,Δq:isProp(B(x))Γ,Δx:A.ϕ B(x)prop\frac{\Gamma, \Delta \vdash \left[\sum_{x:A} B(x)\right] \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash q:\mathrm{isProp}(B(x))}{\Gamma, \Delta \vdash \exists x:A.\phi_B(x) \; \mathrm{prop}}

The rules above reflect the propositions as some types philosophy in type theory.

Bounded separation

A predicate on a type AA is a proposition PpropP \; \mathrm{prop} in the context of the free variable x:Ax:A. Bounded separation states that given a predicate PP on a set AA, one could construct the set |P|\vert P \vert with an injection i:|P|Ai:\vert P \vert \hookrightarrow A

ΓAtypeΓ,x:APpropΓ|P|type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash P \; \mathrm{prop}}{\Gamma \vdash \vert P \vert \; \mathrm{type}}
ΓAtypeΓ,x:APpropΓi:|P|A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash P \; \mathrm{prop}}{\Gamma \vdash i:\vert P \vert \to A}
ΓAtypeΓ,x:APpropΓ,x:A,y:Aφ x= Ayφi(x)= Bi(y)true\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash P \; \mathrm{prop}}{\Gamma, x:A, y:A \vdash \varphi_{x =_A y} \iff \varphi{i(x) =_B i(y)} \; \mathrm{true}}
ΓAtypeΓ,xAPpropΓ,xAP(x)φ y:|P|i(y)=xtrue\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x \in A \vdash P \; \mathrm{prop}}{\Gamma, x \in A \vdash P(x) \iff \varphi_{\sum_{y:\vert P \vert} i(y) = x} \; \mathrm{true}}

Propositions as types

An alternative to the propositions as some types philosophy is the propositions as types philosophy, where instead of reflecting the subsingletons to propositions and the singletons to true propositions, we reflect all types to propositions, and the pointed types to true propositions. The rules are given as follows:

ΓAtypeΓϕ ApropΓAtypeΓa:AΓϕ Atrue\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \phi_A \; \mathrm{prop}} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A}{\Gamma \vdash \phi_A \; \mathrm{true}}

and similar rules for predicates:

Γ,x:A,ΔBtypeΓ,x:A,Δϕ BpropΓ,x:A,ΔBtypeΓ,x:A,Δb:BΓ,x:A,Δϕ Btrue\frac{\Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, x:A, \Delta \vdash \phi_B \; \mathrm{prop}} \qquad \frac{\Gamma, x:A, \Delta \vdash B \; \mathrm{type} \quad \Gamma, x:A, \Delta \vdash b:B}{\Gamma, x:A, \Delta \vdash \phi_B \; \mathrm{true}}

There is no need for propositional truncations in this interpretation: the full intuitionistic logic results from reflecting all type formers except for the natural numbers type and identity types:

ΓA+BtypeΓϕ Aϕ Bprop\frac{\Gamma \vdash A + B \; \mathrm{type}}{\Gamma \vdash \phi_A \vee \phi_B \; \mathrm{prop}}
ΓA×BtypeΓϕ Aϕ Bprop\frac{\Gamma \vdash A \times B \; \mathrm{type}}{\Gamma \vdash \phi_A \wedge \phi_B \; \mathrm{prop}}
ΓABtypeΓϕ Aϕ Bprop\frac{\Gamma \vdash A \to B \; \mathrm{type}}{\Gamma \vdash \phi_A \implies \phi_B \; \mathrm{prop}}
Γ𝟘typeΓpropΓ𝟙typeΓprop\frac{\Gamma \vdash \mathbb{0} \; \mathrm{type}}{\Gamma \vdash \bot \; \mathrm{prop}} \qquad \frac{\Gamma \vdash \mathbb{1} \; \mathrm{type}}{\Gamma \vdash \top \; \mathrm{prop}}
Γ x:AB(x)typeΓx:A.ϕ B(x)prop\frac{\Gamma \vdash \sum_{x:A} B(x) \; \mathrm{type}}{\Gamma \vdash \exists x:A.\phi_B(x) \; \mathrm{prop}}
Γ x:AB(x)typeΓx:A.ϕ B(x)prop\frac{\Gamma \vdash \prod_{x:A} B(x) \; \mathrm{type}}{\Gamma \vdash \forall x:A.\phi_B(x) \; \mathrm{prop}}

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:

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 April 17, 2024 at 11:05:06. See the history of this page for a list of all contributions to it.