Martin-Löf type theory (MLTT)

The characterisation Martin-Löf type theory (MLTT) refers to a family of type theories that originated in the work of Per Martin-Löf. MLTTs are also known as constructive type theories, or intuitionistic type theories.

MLTTs have some common characteristics:

• they are dependent
• they are predicative
• they feature identity types
• and (optionally) universes.

Depending on whether the identity types are intensional or extensional, MLTTs can be classified into two basic systems:

• Intensional Type Theory
• Extensional Type Theory

Irrespective of what kind of identity types they have, MLTTs usually come equipped with two basic type constructors: dependent sums and dependent products.

Dependent sums

Dependent sums (or, colloquially, sigmas) are formed by the rule

\frac{
  \Gamma , x : A \vdash B \textsf{ type}
}{
	\Gamma \vdash (x : A) \times B \textsf{ type}
}

Elements of the dependent sum type are formed by pairing:

\frac{
	\Gamma \vdash a : A
  \quad
  \Gamma, x : A \vdash B \textsf{ type}
  \quad
  \Gamma \vdash b : B[a/x]
}{
	\Gamma \vdash (a, b) : (x : A) \times B
}

A term of dependent sum type is eliminated by projecting its components:

\frac{
	\Gamma \vdash M : (x : A) \times B
}{
  \Gamma \vdash \pi_1(M) : A
}
\quad
\frac{
	\Gamma \vdash M : (x : A) \times B
}{
  \Gamma \vdash \pi_2(M) : B[\pi_1(M)/x]
}

There are associated computation (\beta) and uniqueness (\eta) laws.

Bear in mind that there are slightly differing formulations of dependent sum types, which differ in strength: see §11.4 in Jacobs 1999.

Sums have historically been notated as either \sum_{x : A} B(x) or \Sigma x : A.\ B. The notation used here has been introduced in the 2010s as a shorthand.

Dependent products

Dependent products (or, colloquially, pis) are formed by the rule

\frac{
  \Gamma , x : A \vdash B \textsf{ type}
}{
	\Gamma \vdash (x : A) \to B \textsf{ type}
}

Elements of the dependent product are functions, which are formed by \lambda-abstraction.

\frac{
  \Gamma, x : A \vdash M : B
}{
	\Gamma \vdash \lambda x : A. M : (x : A) \to B
}

To eliminate a function, apply it to an argument:

\frac{
	\Gamma \vdash M : (x : A) \to B
  \quad
  \Gamma \vdash N : A
}{
  \Gamma \vdash MN : B[M/x]
}

Products have historically been notated as either \prod_{x : A} B(x) or \Pi x : A.\ B. The notation used here has been introduced in the 2010s as a shorthand.

References

• A very useful reference article on various dependent type theories, including MLTTs, is the following chapter by Martin Hofmann. It has its origins as a chapter in his thesis. Moreover, it is a very good intro to their categorical semantics.

@incollection{hofmann_1997,
	title = {Syntax and {Semantics} of {Dependent} {Types}},
	url = {https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/pdfs/syntaxandsemanticsof-dependenttypes.pdf},
	booktitle = {Semantics and {Logics} of {Computation}},
	publisher = {Cambridge University Press},
	author = {Hofmann, Martin},
	editor = {Pitts, Andrew M. and Dybjer, P.},
	year = {1997},
	doi = {10.1017/CBO9780511526619.004},
	pages = {79--130}
}

• An introductory book on Martin-Löf type theory is

@book{nordstrom_programming_1990,
	title = {Programming in {Martin}-{L\"{o}f}'s {Type} {Theory}: an {Introduction}},
	isbn = {0-19-853814-6},
	url = {http://www.cse.chalmers.se/research/group/logic/book/},
	publisher = {Oxford University Press},
	author = {Nordström, Bengt and Petersson, Kent and Smith, Jan M.},
	year = {1990},
	doi = {10.1016/0377-0427(91)90052-L}
}

(The title is deceptive; there is almost no programming in that book.)

• The first article on Martin-Löf type theory is

This presents Intensional Type Theory, and remained unpublished until it was included in a 1998 volume.

• There is an entry in the Stanford encyclopedia of philosophy.

• A categorical semantics for MLTTs in terms of comprehension categories is formulated in chapter 11 of

@book{jacobs_categorical_1999,
	address = {Amsterdam},
	series = {Studies in {Logic} and the {Foundations} of {Mathematics}},
	title = {Categorical {Logic} and {Type} {Theory}},
	number = {141},
	publisher = {North Holland},
	author = {Jacobs, Bart},
	year = {1999}
}