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.
In dependent type theory, and particularly homotopy type theory, an identification is a word sometimes used for an inhabitant of an identity type. Alternatives to the term identification include identity, path, or equality, though those phrases are also used in different contexts.
Thus an identification provides a “reason”, a “witness”, or a “proof” that and “are equal”, or more precisely a way in which to identify them. one can say that and are identified. The distinguishing feature of homotopy type theory is that in general, there may be more than one way to identify two things, i.e. more than one identification between two given elements.
One also has identity types of arbitrary arity indexed by given index type , instead of the usual identity types for two elements . The elements of these identity types are also called identifications, or identifications of arbitrary arity.
If the index type is the standard finite type with elements , then is called the n-ary identity type and elements of said type can be called -ary identifications. For , these result in the usual notion of binary identificaiton.
Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082)
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Last revised on July 3, 2025 at 17:09:19. See the history of this page for a list of all contributions to it.