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
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
By intensional type theory one means the flavor of type theory in which identity types are not forced to be judgmental equalities by equality reflection.
The original definition of identity types in Martin-Löf dependent type theory [Martin-Löf (1975, §1.7 and p. 94)] is by default intensional: It takes an additional axiom or rule — the identity reflection rule, cf. Streicher (1993, p. 4, 13 ); Hofmann (1995, p. 16) — to turn intensional into extensional type theory (in which identity types are then turned into judgmental equality).
In particular,
homotopy type theory is intensional: the categorical semantics of its identity types are path space objects.
Any theory with UIP or axiom K but no equality reflection is an intensional set-level type theory
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)
Thomas Streicher, Investigations into Intensional Type Theory, Habilitation Thesis, Darmstadt (1993) [pdf, pdf]
Martin Hofmann, Extensional concepts in intensional type theory, Ph.D. thesis, University of
Edinburgh, (1995) (ECS-LFCS-95-327, pdf)
Intensional type theory is discussed in chapter 4 of:
Last revised on May 17, 2025 at 13:47:00. See the history of this page for a list of all contributions to it.