[[!redirects Martin-Löf Intensional 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 $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 #### category: type theory