type theories (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