Intensional Type Theory

Intensional type theory (ITT) is a Martin-Löf type theory.

At its core, ITT is the type theory equipped with \Pi, \Sigma and intensional identity types.

ITT is a particularly well-behaved system, as its type checking problem is decidable. This is in contrast to extensional type theory.

Intensional identity types

We can form intensional identity types by

\frac{
	\Gamma \vdash A \textsf{ type}
  \quad
  \Gamma \vdash M : A
  \quad
  \Gamma \vdash N : A
}{
	\Gamma \vdash \textsf{Id}_A(M, N) \textsf{ type}
}

There is one constructor, the reflexivity:

\frac{
  \Gamma \vdash M : A
}{
	\Gamma \vdash \textsf{refl}_A(M) : \textsf{Id}_A(M, N)
}

The elimination form for the intensional version of the identity type takes a very particular form, which is known as the \textsf{J} eliminator.

\frac{
	\Gamma \vdash P : \textsf{Id}_A(M, N)
  \quad
  \Gamma, x : A, y : A, p : \textsf{Id}_A(x, y) \vdash C \textsf{ type}
  \quad
  \Gamma, z : A \vdash X : C[z, z, \textsf{refl}_A(z)/x, y, p]
}{
	\Gamma \vdash \textsf{J}_{[x, y, p. C]}(M, N, P, X) : C[M, N, P/x, y, p]
}

Following the development of HoTT, this rule has also been referred to as path induction.

Extensions

ITT is not a particularly strong system. In fact, it does not prove a number of extensionality axioms.

Please expand.

Homotopy type theory

The extension of ITT with the Univalence axiom is known as (book) HoTT.

See also

• Martin-Löf type theory
• Observational type theory

References

• 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.

• Further improvements (predicative part) were presented in ...

• There is also a nLab page on ITT.

• Streicher discusses a number of 'criteria of intensionality' (in the old sense) of ITT in

@inproceedings{streicher_2015,
	address = {Cham},
	series = {Research {Perspectives} {CRM} {Barcelona}},
	title = {How {Intensional} {Is} {Homotopy} {Type} {Theory}?},
	doi = {10.1007/978-3-319-21284-5_20},
	booktitle = {Extended {Abstracts} {Fall} 2013: {Geometrical} {Analysis}; {Type} {Theory}, {Homotopy} {Theory} and {Univalent} {Foundations}},
	publisher = {Birkhäuser Basel},
	author = {Streicher, Thomas},
	editor = {González, Maria del Mar and Yang, Paul C. and Gambino, Nicola and Kock, Joachim},
	year = {2015},
	pages = {105--110}