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.
basic constructions:
strong axioms
further
In dependent type theory, the term typal equality is used to describe the use of the identity type to represent the notion of equality of terms, and is primarily used to distinguish from the notion of judgmental equality of terms.
In dependent type theories with a separate proposition judgment $\phi \mathrm{prop}$, the term typal equality is also used to distinguish identity types from propositional equality, which is the equality judged to be a proposition; i.e. $a =_A b \mathrm{prop}$. On the other hand, in dependent type theory without a separate proposition judgment, propositions are usually defined to be certain types, and the term “propositional equality” is used as a synonym of typal equality in referring to identity types. (In fact, “propositional equality” is the older and arguably still more common term in this context.)
Last revised on January 14, 2024 at 06:39:58. See the history of this page for a list of all contributions to it.