[[!redirects pointed]] ## 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 $$\mathcal{U}_+\equiv \sum_{X:\mathcal{U}}X$$ ## Properties ## Elements of $\mathcal{U}_+$ are of the form $(X,\star_X)$. There is a way of pointing any type $X$ by forming the sum $X+\mathbf{1}$ and taking $inr(\star_{\mathbf{1}})$ as the base point. ## See also ## * [[Synthetic homotopy theory]] * [[suspension]] ## References ## [[HoTT book]]