Homotopy Type Theory type theories > history (Rev #6)

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.