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

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

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

• Martin-Löf Intensional Type Theory: the original.
• The Calculus Of Constructions?: the basis of Coq.
• The type theory of Agda: apparently has no formal definition other than the Agda source code.
• Vladimir Voevoedsky?Vladimir Voevodsky’s Homotopy Type System