## Idea ## A type theory is a formal system in which every term has a '[[type]]', and operations in the system are restricted to acting on specific types. A number of [[type theories]] have been used or proposed for doing homotopy type theory. ## List of examples ## 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 [[nlab:Coq]] proof assistant. * [[Agda]]: based on Martin-Löf type theory, extended by a flexible scheme for specifying inductive definitions. * [[Homotopy Type System]]: a proposal by Vladimir Voevodsky. * [[Two-level type theory]] * [[cubical type theory]] (which has various forms) ## See also ## '[[nlab:type theory|Type theory]]' on the nLab wiki. [[!redirects type theories]]