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.
A notion of equality in type theory involving the notion of judgement. In homotopy type theory it is used synonymously with definitional equality as contrasted with propositional equality.
Last revised on August 24, 2020 at 10:08:20. See the history of this page for a list of all contributions to it.