Intuitionistic type theory

Intuitionistic type theory is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.

Design

Martin-Löf designed the type theory on the principles of mathematical constructivism. Constructivism requires any existence proof to contain a "witness". So, any proof of "there exists a prime greater than 1000" must identify a specific number that is both prime and greater than 1000. 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.
Intuitionistic type theory's type constructors were built to follow a one-to-one correspondence with logical connectives. For example, the logical connective called implication corresponds to the type of a function. This correspondence is called the Curry–Howard isomorphism. Prior type theories had also followed this isomorphism, but Martin-Löf's was the first to extend it to predicate logic by introducing dependent types.

Type theory

A type theory is a kind of mathematical ontology, or foundation, describing the fundamental objects that exist. In the standard foundation, set theory combined with mathematical logic, the fundamental object is the set, which is a container that contains elements. In type theory, the fundamental object is the term, each of which belongs to one and only one type.
Intuitionistic type theory has three finite types, which are then composed using five different type constructors. Unlike set theories, type theories are not built on top of a logic like Frege's. So, each feature of the type theory does double duty as a feature of both math and logic.

0 type, 1 type and 2 type

There are three finite types: The 0 type contains no terms. The 1 type contains one canonical term. The 2 type contains two canonical terms.
Because the 0 type contains no terms, it is also called the empty type. It is used to represent anything that cannot exist. It is also written and represents anything unprovable. As a result, negation is defined as a function to it:.
Likewise, the 1 type contains one canonical term and represents existence. It also is called the unit type.
Finally, the 2 type contains two canonical terms. It represents a definite choice between two values. It is used for Boolean values but not propositions.
Propositions are instead represented by particular types. For instance, a true proposition can be represented by the 1 type, while a false proposition can be represented by the 0 type. But we cannot assert that these are the only propositions, i.e. the law of excluded middle does not hold for propositions in intuitionistic type theory.

Σ type constructor

Σ-types contain ordered pairs. As with typical ordered pair types, a Σ-type can describe the Cartesian product,, of two other types, and. Logically, such an ordered pair would hold a proof of and a proof of, so one may see such a type written as.
Σ-types are more powerful than typical ordered pair types because of dependent typing. In the ordered pair, the type of the second term can depend on the value of the first term. For example, the first term of the pair might be a natural number and the second term's type might be a sequence of reals of length equal to the first term. Such a type would be written:
Using set-theory terminology, this is similar to an indexed disjoint union of sets. In the case of the usual cartesian product, the type of the second term does not depend on the value of the first term. Thus the type describing the cartesian product is written:
It is important to note here that the value of the first term,, is not dependent on the type of the second term,.
Σ-types can be used to build up longer dependently-typed tuples used in mathematics and the records or structs used in most programming languages. An example of a dependently-typed 3-tuple is two integers and a proof that the first integer is smaller than the second integer, described by the type:
Dependent typing allows Σ-types to serve the role of existential quantifier. The statement "there exists an of type, such that is proven" becomes the type of ordered pairs where the first item is the value of type and the second item is a proof of. Notice that the type of the second item depends on the value in the first part of the ordered pair. Its type would be:

Π type constructor

Π-types contain functions. As with typical function types, they consist of an input type and an output type. They are more powerful than typical function types however, in that the return type can depend on the input value. Functions in type theory are different from set theory. In set theory, you look up the argument's value in a set of ordered pairs. In type theory, the argument is substituted into a term and then computation is applied to the term.
As an example, the type of a function that, given a natural number, returns a vector containing real numbers is written:
When the output type does not depend on the input value, the function type is often simply written with a. Thus, is the type of functions from natural numbers to real numbers. Such Π-types correspond to logical implication. The logical proposition corresponds to the type, containing functions that take proofs-of-A and return proofs-of-B. This type could be written more consistently as:
Π-types are also used in logic for universal quantification. The statement "for every of type, is proven" becomes a function from of type to proofs of. Thus, given the value for the function generates a proof that holds for that value. The type would be

= type constructor

=-types are created from two terms. Given two terms like and, you can create a new type. The terms of that new type represent proofs that the pair reduce to the same canonical term. Thus, since both and compute to the canonical term, there will be a term of the type. 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 where the terms do not reduce to the same canonical term, but you will be unable to create terms of that new type. In fact, if you were able to create a term of, you could create a term of. Putting that into a function would generate a function of type. Since is how intuitionistic type theory defines negation, you would have or, finally,.
Equality of proofs is an area of active research in proof theory and has led to the development of homotopy type theory and other type theories.

Inductive types

Inductive types allow the creation of complex, self-referential types. For example, a linked list of natural numbers is either an empty list or a pair of a natural number and another linked list. Inductive types can be used to define unbounded mathematical structures like trees, graphs, etc.. In fact, the natural numbers type may be defined as an inductive type, either being or the successor of another natural number.
Inductive types define new constants, such as zero and the successor function. Since does not have a definition and cannot be evaluated using substitution, terms like and become the canonical terms of the natural numbers.
Proofs on inductive types are made possible by induction. Each new inductive type comes with its own inductive rule. To prove a predicate for every natural number, you use the following rule:
Inductive types in intuitionistic type theory are defined in terms of W-types, the type of well-founded trees. Later work in type theory generated coinductive types, induction-recursion, and induction-induction for working on types with more obscure kinds of self-referentiality. Higher inductive types allow equality to be defined between terms.

Universe types

The universe types allow proofs to be written about all the types created with the other type constructors. Every term in the universe type can be mapped to a type created with any combination of and the inductive type constructor. However, to avoid paradoxes, there is no term in that maps to for any.
To write proofs about all "the small types" and, you must use, which does contain a term for, but not for itself. Similarly, for. There is a predicative hierarchy of universes, so to quantify a proof over any fixed constant universes, you can use.
Universe types are a tricky feature of type theories. Martin-Löf's original type theory had to be changed to account for Girard's paradox. Later research covered topics such as "super universes", "Mahlo universes", and impredicative universes.

Judgements

The formal definition of intuitionistic type theory is written using judgements. For example, in the statement "if is a type and is a type then is a type" there are judgements of "is a type", "and", and "if... then...". The expression is not a judgement; it is the type being defined.
This second level of the type theory can be confusing, particularly where it comes to equality. There is a judgement of term equality, which might say. It is a statement that two terms reduce to the same canonical term. There is also a judgement of type equality, say that, which means every element of is an element of the type and vice versa. At the type level, there is a type and it contains terms if there is a proof that and reduce to the same value. Lastly, there is an English-language level of equality, because we use the word "four" and symbol "" to refer to the canonical term. Synonyms like these are called "definitionally equal" by Martin-Löf.
The description of judgements below is based on the discussion in Nordström, Petersson, and Smith.
The formal theory works with types and objects.
A type is declared by:

An object exists and is in a type if:

Objects can be equal

and types can be equal

A type that depends on an object from another type is declared

and removed by substitution

, replacing the variable with the object in.

An object that depends on an object from another type can be done two ways.
If the object is "abstracted", then it is written

and removed by substitution

, replacing the variable with the object in.

The object-depending-on-object can also be declared as a constant as part of a recursive type. An example of a recursive type is:

Here, is a constant object-depending-on-object. It is not associated with an abstraction. Constants like can be removed by defining equality. Here the relationship with addition is defined using equality and using pattern matching to handle the recursive aspect of :
is manipulated as an opaque constant - it has no internal structure for substitution.
So, objects and types and these relations are used to express formulae in the theory. The following styles of judgements are used to create new objects, types and relations from existing ones:

	σ is a well-formed type in the context Γ.
	t is a well-formed term of type σ in context Γ.
	σ and τ are equal types in context Γ.
	t and u are judgmentally equal terms of type σ in context Γ.
	Γ is a well-formed context of typing assumptions.

By convention, there is a type that represents all other types. It is called . Since is a type, the members of it are objects. There is a dependent type that maps each object to its corresponding type. In most texts is never written. From the context of the statement, a reader can almost always tell whether refers to a type, or whether it refers to the object in that corresponds to the type.
This is the complete foundation of the theory. Everything else is derived.
To implement logic, each proposition is given its own type. The objects in those types represent the different possible ways to prove the proposition. If there is no proof for the proposition, then the type has no objects in it. Operators like "and" and "or" that work on propositions introduce new types and new objects. So is a type that depends on the type and the type. The objects in that dependent type are defined to exist for every pair of objects in and. If either or have no proof and is an empty type, then the new type representing is also empty.
This can be done for other types and their operators.