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 theory which fails to satisfy function extensionality. This is in general an orthogonal requirement to how we are using the term here.
Only the intensional but not the extensional Martin-Löf type theory has decidable type checking. (Martin-Löf, Hofmann).
Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium ‘73
(Amsterdam) (H. E. Rose and J. C. Shepherdson, eds.), North-Holland, 1975, pp. 73-118.
Martin Hofmann, Extensional concepts in intensional type theory, Ph.D. thesis, University of
Edinburgh, (1995) (web)
Last revised on January 16, 2019 at 19:02:53. See the history of this page for a list of all contributions to it.