Homotopy Type Theory
pointed type (Rev #2)


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.


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

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


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


HoTT book

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