Homotopy Type Theory
Martin-Löf Type Theory

Idea

A type theory created by Per Martin-Löf in 1972. Martin-Löf created both intensional and extensional variants.

Syntax

The syntax of Martin-Löf 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 four basic judgement forms:

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

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

The four judgements are inductively defined by the following inference rules.

Inference rules

Structural rules

Logical constructors

Π\Pi-types

Σ\Sigma-types

Identity types

Intentional or extensional?

W-types

TODO: link to page on W-types, Indexed W-types, etc.

Empty type

Unit type

Sum type

Universes

a la Tarski

Further rules

η\eta for Π\Pi-types

Function extensionality

category: type theory

Last revised on May 27, 2020 at 15:20:22. See the history of this page for a list of all contributions to it.