Homotopy Type Theory
type theories > history (Rev #4, changes)
Showing changes from revision #3 to #4:
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.
- 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 02:20:14 by
Alexis Hazell?.
See the history of this page for a list of all contributions to it.