Intensional type theory (ITT) is a Martin-Löf type theory.
At its core, ITT is the type theory equipped with , 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.
We can form intensional identity types by
There is one constructor, the reflexivity:
The elimination form for the intensional version of the identity type takes a very particular form, which is known as the eliminator.
Following the development of HoTT, this rule has also been referred to as path induction.
ITT is not a particularly strong system. In fact, it does not prove a number of extensionality axioms.
Please expand.
The extension of ITT with the Univalence axiom is known as (book) HoTT.
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.
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
Streicher, Thomas. 2015. ‘How Intensional Is Homotopy Type Theory?’ In Extended Abstracts Fall 2013: Geometrical Analysis; Type Theory, Homotopy Theory and Univalent Foundations, edited by Maria del Mar González, Paul C. Yang, Nicola Gambino, and Joachim Kock, 105–110. Research Perspectives CRM Barcelona. Cham: Birkhäuser Basel. https://doi.org/10.1007/978-3-319-21284-5_20.
@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}