Homotopy Type Theory type theories > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

This page is lists a some list of the type theories and their variations that have been used or proposed for doing homotopy type theory theory. / univalent foundations.

• 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 Coq. the Coq proof assistant.
• The type theory of Agda : apparently based has on no Martin-Löf formal type definition theory, other extended than by the a Agda flexible source scheme code. for specifying inductive definitions.
• Vladimir Voevodsky’s Homotopy Type System: work in progress based on a proposal by Vladimir Voevodsky.