Showing changes from revision #1 to #2:
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.
Revision on October 10, 2018 at 23:09:25 by Ali Caglayan. See the history of this page for a list of all contributions to it.