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
In dependent type theory, an identity system is a correspondence on a type $A$
which behaves like a weak identity type on $A$.
Identity systems are very useful in characterizing the extensionality principle of types such as function types, dependent function types, and Tarski universes.
In dependent type theory, an identity system on a type $A$ is a correspondence on $A$, $a:A, b:A \vdash R(a, b)$, with a dependent function
such that for any family of types
there exists a dependent function
and a dependent function
product extensionality states that the correspondence
is an identity system.
dependent pair extensionality states that the correspondence
is an identity system.
function extensionality states that the correspondence
is an identity system.
dependent function extensionality states that the correspondence
is an identity system.
univalence or universe extensionality states that the correspondence
is an identity system.
Univalent Foundations Project, Def. 5.8.3 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]
Egbert Rijke, Def. 11.2.1 in: Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (2023) [arXiv:2212.11082]
Last revised on January 30, 2023 at 16:02:57. See the history of this page for a list of all contributions to it.