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

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 Voevodsky’s Homotopy Type System