Homotopy Type Theory
type theory (changes)

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

List of examples

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

• The system presented known in asBook 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.