# Homotopy Type Theory pointed type (Rev #1)

## 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.

## References

HoTT book

Revision on September 4, 2018 at 09:52:49 by Ali Caglayan. See the history of this page for a list of all contributions to it.