natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Intensional type theory is the flavor of type theory in which identity types are not necessarily propositions (that is, (-1)-truncated). Martin-Löf‘s original definition of identity types, and the equivalent formulation as an inductive type, are by default “intensional”; one has to impose extra axioms or rules in order to get extensional type theory (in which identity types are propositions).
In particular, homotopy type theory is intensional, because identity types represent path objects.
Note that some type theorists use “intensional type theory” to refer to type theories which fail to satisfy function extensionality. This is in general an orthogonal requirement to how we are using the term here.
The origin of the names “extensional” and “intensional” is somewhat confusing. In fact they refer to the behavior of the definitional equality. The idea is that the identity type is always an “extensional” notion of equality (although it can be more or less extensional, depending on whether further extensionality principles like function extensionality and univalence hold). Thus, if the definitional equality coincides with the identity type, the former is also extensional, and so we call the type theory “extensional” — while if the two equalities do not coincide, then the definitional equality has room to be more intensional than the identity type, and so we call the type theory “intensional”. (On this historical reading, “extensional type theory” should refer only to definitionally extensional type theory with the reflection rule, which is much stronger than merely requiring all types to be h-sets.)
Only the intensional but not the extensional Martin-Löf type theory has decidable type checking. (Martin-Löf 75, Hofmann 95).
Per Martin-Löf, An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 Pages 73-118, Elsevier 1975 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)
Martin Hofmann, Extensional concepts in intensional type theory, Ph.D. thesis, University of
Edinburgh, (1995) (ECS-LFCS-95-327, pdf)
Last revised on September 1, 2022 at 05:09:09. See the history of this page for a list of all contributions to it.