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
basic constructions:
strong axioms
further
The homotopy type theory presented in the HoTT book.
Book homotopy type theory or Book HoTT is a Martin-Löf univalent type theory with all the additional types mentioned in the HoTT book:
Last revised on June 6, 2022 at 21:41:35. See the history of this page for a list of all contributions to it.