Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972.
However, all versions keep the core design of constructive logic using dependent types.
Martin-Löf designed the type theory on the principles of mathematical constructivism.
Intuitionistic type theory accomplished this design goal by internalizing the BHK interpretation.
A useful consequence is that proofs become mathematical objects that can be examined, compared, and manipulated.
As with typical ordered pair (or 2-tuple) types, a Σ-type can describe the Cartesian product,
Such a type would be written: Using set-theory terminology, this is similar to an indexed disjoint union of sets.
Σ-types can be used to build up longer dependently-typed tuples used in mathematics and the records or structs used in most programming languages.
This type could be written more consistently as: Π-types are also used in logic for universal quantification.
In intuitionistic type theory, there is a single way to introduce =-types and that is by reflexivity: It is possible to create =-types such as
Inductive types can be used to define unbounded mathematical structures like trees, graphs, etc..
Higher inductive types allow equality to be defined between terms.
There is a predicative hierarchy of universes, so to quantify a proof over any fixed constant
Martin-Löf's original type theory had to be changed to account for Girard's paradox.
The formal definition of intuitionistic type theory is written using judgements.
The description of judgements below is based on the discussion in Nordström, Petersson, and Smith.
If the object is "abstracted", then it is written and removed by substitution The object-depending-on-object can also be declared as a constant as part of a recursive type.
Here the relationship with addition is defined using equality and using pattern matching to handle the recursive aspect of
Using the language of category theory, R. A. G. Seely introduced the notion of a locally cartesian closed category (LCCC) as the basic model of type theory.
A theory such as that of predicative set theory expresses closure conditions on the types of sets and their elements: that they should be closed under operations that reflect dependent sum and product, and under various forms of inductive definition.
In contrast, in intensional type theory type checking is decidable, but the representation of standard mathematical concepts is somewhat more cumbersome, since intensional reasoning requires using setoids or similar constructions.
Integers and rational numbers can be represented without setoids, but this representation is difficult to work with.
Different forms of type theory have been implemented as the formal systems underlying a number of proof assistants.
While many are based on Per Martin-Löf's ideas, many have added features, more axioms, or a different philosophical background.
Dependent types also feature in the design of programming languages such as ATS, Cayenne, Epigram, Agda,[6] and Idris.
[7] Per Martin-Löf constructed several type theories that were published at various times, some of them much later than when the preprints with their description became accessible to specialists (among others Jean-Yves Girard and Giovanni Sambin).
Jean-Yves Girard has shown that this system was inconsistent, and the preprint was never published.
The universe was "predicative" in the sense that the dependent product of a family of objects from V over an object that was not in V such as, for example, V itself, was not assumed to be in V. The universe was à la Russell's Principia Mathematica, i.e., one would write directly "T∈V" and "t∈T" (Martin-Löf uses the sign "∈" instead of modern ":") without an added constructor such as "El".
In fact, Corollary 3.10 on p. 115 says that if A∈Vm and B∈Vn are such that A and B are convertible then m = n. This means, for example, that it would be difficult to formulate univalence axiom in this theory—there are contractible types in each of the Vi, but it is unclear how to declare them to be equal since there are no identity types connecting Vi and Vj for i ≠ j. MLTT79 was presented in 1979 and published in 1982.
There are identity types with the J-eliminator (which already appeared in MLTT73 but did not have this name there) but also with the rule that makes the theory "extensional" (p. 169).