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:
Depending on whether the identity types are intensional or extensional, MLTTs can be classified into two basic systems:
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 (or, colloquially, sigmas) are formed by the rule
Elements of the dependent sum type are formed by pairing:
A term of dependent sum type is eliminated by projecting its components:
There are associated computation () and uniqueness () 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 or . The notation used here has been introduced in the 2010s as a shorthand.
Dependent products (or, colloquially, pis) are formed by the rule
Elements of the dependent product are functions, which are formed by -abstraction.
To eliminate a function, apply it to an argument:
Products have historically been notated as either or . The notation used here has been introduced in the 2010s as a shorthand.
Hofmann, Martin. 1997. ‘Syntax and Semantics of Dependent Types’. In Semantics and Logics of Computation, edited by Andrew M. Pitts and P. Dybjer, 79–130. Cambridge University Press. https://doi.org/10.1017/CBO9780511526619.004. pdf
@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}
}
Nordström, Bengt, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-Löf’s Type Theory: An Introduction. Oxford University Press. https://doi.org/10.1016/0377-0427(91)90052-L. [pdf]
@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.)
Martin-Löf, Per. 1972. 'An Intuitionistic Theory of Types'. pdf
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
Jacobs, Bart. 1999. Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. Amsterdam: North Holland.
@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}
}