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]]