Homotopy Type Theory
pointed type

Idea

For many theorems about types (especially in homotopy theory) we need them to at least have a single element for which to perform constructions such as loop spaces on. This leads to a notion of pointed types. This can be thought of the constructive version of being non-empty.

Defintion

For a given type universe 𝒰\mathcal{U} the type of pointed types is

𝒰 + X:𝒰X\mathcal{U}_+\equiv \sum_{X:\mathcal{U}}X

Properties

Elements of 𝒰 +\mathcal{U}_+ are of the form (X, X)(X,\star_X). There is a way of pointing any type XX by forming the sum X+1X+\mathbf{1} and taking inr( 1)inr(\star_{\mathbf{1}}) as the base point.

See also

References

HoTT book

Last revised on October 10, 2018 at 19:09:25. See the history of this page for a list of all contributions to it.