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.