[[!redirects empty]] _"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]] category: type theory