This page lists some of the type theories and variations that have been used or proposed for doing homotopy type theory. * The system presented in [[the HoTT book]], chapter 1 and appendix A. * [[Martin-Löf Type Theory|Martin-Löf Intensional Type Theory]]: the original. * The [[Calculus Of Constructions]]: the basis of the [[Coq]] proof assistant. * [[Agda]]: based on Martin-Löf type theory, extended by a flexible scheme for specifying inductive definitions. * [[Homotopy Type System]]: work in progress based on a proposal by Vladimir Voevodsky.