## 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 types in HoTT ## Typically types come with four sets of inference rules. Rules allow one to conclude one set of judgements from others. A collection of judgements is typically called a context. * [[function type]] $A \to B$ * [[pi type]] $\prod_{a:A}B$ * [[universe]] $\mathcal{U}$ * [[product type]] $A \times B$ * [[sigma type]] $\sum_{a:A}B$ * [[zero type]] * [[unit type]] ## List of axioms in HoTT ## * [[univalence]] * [[function extensionality]] * [[propositional resizing]] See [[axioms]] --- # Old page # ## 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]] category: type theory