Homotopy Type Theory type theory > history (changes)

Showing changes from revision #10 to #11: Added | Removed | Changed

List of examples

< type theory

This page lists some of the type theories and variations that have been used or proposed for doing homotopy type theory.

  • The system known as Book HoTT presented in the HoTT book, chapter 1 and appendix A.
  • Martin-Löf Intensional Type Theory: the original.
  • The Calculus Of Constructions?: the basis of the Coq proof assistant.
  • Agda: based on Martin-Löf type theory, extended by a flexible scheme for specifying inductive definitions.
  • Homotopy Type System: a proposal by Vladimir Voevodsky.
  • Two-level type theory?
  • cubical type theory? (which has various forms)

See also

Type theory’ on the nLab wiki.

category: type theory

Last revised on June 9, 2022 at 16:41:46. See the history of this page for a list of all contributions to it.