Showing changes from revision #2 to #3:
Added | Removed | Changed
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 the type of pointed types is
Elements of are of the form . There is a way of pointing any type by forming the sum and taking as the base point.