Homotopy Type Theory type > history (Rev #9)

“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

category: type theory

Revision on May 11, 2022 at 02:50:02 by Anonymous?. See the history of this page for a list of all contributions to it.