[[!redirects type]] _"A type is defined as the range of significance of a propositional function, i.e., as the collection of arguments for which the said function has values." -- Bertrand Russell, 1908_ ## 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. Here we will describe the types present in "Book HoTT", the type theory given in the [[HoTT Book]]. All types are seen as elements of a type called $\mathcal{U}$. This is the [[universe]] type. Due to Russel-like paradoxes, we cannot have $\mathcal{U} : \mathcal{U}$, therefore we have an infinite hierarchy of universes $$\mathcal{U}_1 : \mathcal{U}_2 : \mathcal{U}_3 : \dots$$ for every $n$. For most cases it will not matter what universe we are in. ## Function types ## Given a type $A$ and $B$, there is a type $A \to B$ called the [[function type]] representing the type of functions from $A$ to $B$. A function can be defined explicitly using lambda notation $\lambda x . y$. There is a computation rule saying there is a reduction $(\lambda x . y ) a \equiv y[a / x]$ for some $a : A$. The notation $y[a / x]$ means to replace all occurances of $x$ with $a$ in $y$, giving us a term of $B$. ## Pi types ## (...) ## Pair types ## (...) ## Sigma types ## (...) ## References ## * [[HoTT Book]] * [[On the homotopy groups of spheres in 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