Showing changes from revision #12 to #13:
Added | ~~Removed~~ | ~~Chan~~ged

<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*

category: redirected to nlab

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.

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.

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.

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)$

(…)

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)$

(…)

(…)

(…)

(…)

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$

category: not redirected to nlab yet

Last revised on June 16, 2022 at 16:37:42. See the history of this page for a list of all contributions to it.