Homotopy Type Theory type > history (changes)

Showing changes from revision #12 to #13: Added | Removed | Changed

<“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, 1908type

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:𝒰 n:𝒰 s(n)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:𝒰X:\mathcal{U}, i.e. X:𝒰𝒯(X)typeX:\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:𝒰(n)typen:\mathbb{N} \vdash \mathcal{U}(n)\ \mathrm{type}
n:𝒰 (n):𝒰(s(n))n:\mathbb{N} \vdash \mathcal{U}^\prime(n):\mathcal{U}(s(n))
n:𝒯 s(n)(𝒰 (n))𝒰(n)typen:\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 AA and BB, there is a type ABA \to B called the function type representing the type of functions from AA to BB. A function can be defined explicitly using lambda notation λx.y\lambda x . y. There is a computation rule saying there is a reduction (λx.y)ay[a/x](\lambda x . y ) a \equiv y[a / x] for some a:Aa : A. The notation y[a/x]y[a / x] means to replace all occurances of xx with aa in yy, giving us a term of BB.

Universes are closed under function types, i.e.

n:,A:𝒰(n),B:𝒰(n)(A 𝒰(n)B):𝒰(n)n:\mathbb{N}, A: \mathcal{U}(n), B: \mathcal{U}(n) \vdash (A \to_{\mathcal{U}(n)} B) : \mathcal{U}(n)

and

𝒯(n)(A 𝒰(n)B)𝒯(n)(A)𝒯(n)(B)\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 AA and BB, there is a type A×BA \times B called the pair type? or product type? representing the type of pairs (a,b)(a, b) for a:Aa:A and b:Bb:B.

Universes are closed under pair types, i.e.

n:,A:𝒰(n),B:𝒰(n)(A× 𝒰(n)B):𝒰(n)n:\mathbb{N}, A: \mathcal{U}(n), B: \mathcal{U}(n) \vdash (A \times_{\mathcal{U}(n)} B) : \mathcal{U}(n)

and

𝒯(n)(A× 𝒰(n)B)𝒯(n)(A)×𝒯(n)(B)\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 AA, BB, and CC, and functions f:CAf:C \to A and g:CAg:C \to A, there is a type A CBA \sqcup_C B called the homotopy pushout type? representing the homotopy pushout of ff and gg.

Special cases of homotopy pushout types include the type of booleans, which is defined as

21 012 \coloneqq 1 \sqcup_0 1

the coproduct type, which is defined as

A+BA 0BA + B \coloneqq A \sqcup_0 B

and the circle type, which is defined as

S 11 21S^1 \coloneqq 1 \sqcup_2 1

References

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