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
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A version of canonicity where the definitional equalities are replaced with identity types.
In the case for the natural numbers type homotopy canonicity states that every natural number $n:\mathbb{N}$ comes with a natural number $m:\mathbb{N}$ and an identification to the canonical form $p:n =_\mathbb{N} \mathrm{succ}^m(0)$.
Chris Kapulkin and Christian Sattler have an unpublished proof that homotopy type theory has homotopy canonicity, even though HoTT does not have canonicity
cubical type theory has homotopy canonicity
Michael Shulman, Univalence for inverse diagrams, oplax limits, and gluing, and homotopy canonicity (arXiv:1203.3253)
Thierry Coquand, Simon Huber, Christian Sattler, Canonicity and homotopy canonicity for cubical type theory, Logical Methods in Computer Science, Volume 18, Issue 1 (February 3, 2022) lmcs:9043, (doi:10.46298/lmcs-18%281%3A28%292022, arXiv:1902.06572)
Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory (arXiv:2102.00905)
Last revised on December 3, 2023 at 18:14:28. See the history of this page for a list of all contributions to it.