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

Showing changes from revision #0 to #1: 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?’s Homotopy Type System