Homotopy Type Theory Martin-Löf Type Theory > history (Rev #4, changes)

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 $n$ is given by $n$th type in a context.

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

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

We have four basic judgement forms:

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

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

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