[[!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 a typical models of [[homotopy type theory]]. ## Universes ## ### Russell-style universe ### With Russell-style universes, 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]] $$n:\mathbb{N} \vdash \mathcal{U}_n : \mathcal{U}_{s(n)}$$ For most cases it will not matter what universe we are in. ### Tarski-style universe ### With Tarski-style universes, all types are seen as dependent types of a universal type family $\mathcal{T}$ given a type $\mathcal{U}$ called the [[universe]] type and a term $X:\mathcal{U}$, i.e. $X:\mathcal{U} \vdash \mathcal{T}(X) type$. The existence of Russell-like paradoxes means that we similarly cannot have a type $\mathcal{U}^\prime:\mathcal{U}$ such that $\mathcal{T}(\mathcal{U}^\prime) \equiv \mathcal{U}$. Thus, we likewise have an infinite hierarchy of universes $$n:\mathbb{N} \vdash \mathcal{U}(n)\ \mathrm{type}$$ $$n:\mathbb{N} \vdash \mathcal{U}^\prime(n):\mathcal{U}(s(n))$$ $$n:\mathbb{N} \vdash \mathcal{T}_{s(n)}(\mathcal{U}^\prime(n)) \equiv \mathcal{U}(n)\ \mathrm{type}$$ 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$. Universes are closed under function types, i.e. $$n:\mathbb{N}, A: \mathcal{U}(n), B: \mathcal{U}(n) \vdash (A \to_{\mathcal{U}(n)} B) : \mathcal{U}(n)$$ and $$\mathcal{T}(n)(A \to_{\mathcal{U}(n)} B) \equiv \mathcal{T}(n)(A) \to \mathcal{T}(n)(B)$$ ## Pi types ## (...) ## Pair types ## Given a type $A$ and $B$, there is a type $A \times B$ called the [[pair type]] or [[product type]] representing the type of pairs $(a, b)$ for $a:A$ and $b:B$. Universes are closed under pair types, i.e. $$n:\mathbb{N}, A: \mathcal{U}(n), B: \mathcal{U}(n) \vdash (A \times_{\mathcal{U}(n)} B) : \mathcal{U}(n)$$ and $$\mathcal{T}(n)(A \times_{\mathcal{U}(n)} B) \equiv \mathcal{T}(n)(A) \times \mathcal{T}(n)(B)$$ ## Sigma types ## (...) ## Empty type ## (...) ## Unit type ## (...) ## Identity types ## (...) ## Homotopy pushout types ## Given types $A$, $B$, and $C$, and functions $f:C \to A$ and $g:C \to A$, there is a type $A \sqcup_C B$ called the [[homotopy pushout type]] representing the homotopy pushout of $f$ and $g$. Special cases of homotopy pushout types include the type of booleans, which is defined as $$2 \coloneqq 1 \sqcup_0 1$$ the coproduct type, which is defined as $$A + B \coloneqq A \sqcup_0 B$$ and the circle type, which is defined as $$S^1 \coloneqq 1 \sqcup_2 1$$ ## References ## * [[nlab:Introduction to Homotopy Type Theory]] category: not redirected to nlab yet