Showing changes from revision #4 to #5:
Added | Removed | Changed
A type theory created by Per Martin-Löf in 1972. Martin-Löf created both intensional and extensional variants.
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 is given by th type in a context.
One may also define contexts as coming with a variable name, in which case one needs a notion of -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:
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.
Intentional or extensional?
TODO: link to page on W-types, Indexed W-types, etc.
a la Tarski