Homotopy Type Theory
type theories (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

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

  • The system 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.Coq? proof assistant.
  • Agda: based on Martin-Löf type theory, extended by a flexible scheme for specifying inductive definitions.
  • Homotopy Type System: work in progress based on a proposal by Vladimir Voevodsky.

Revision on May 9, 2014 at 22:03:17 by Alexis Hazell?. See the history of this page for a list of all contributions to it.