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)
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, and is primarily used to distinguish from the notion of judgmental equality.
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 September 15, 2023 at 15:09:10. See the history of this page for a list of all contributions to it.