nLab reduced suspension type

Idea

In homotopy type theory, the notion of reduced suspension type is an axiomatization of the reduced suspension in pointed homotopy theory.

The underlying type of a pointed reduced suspension type is equivalent to the plain suspension type of the given underlying type, so that, up to equivalence one may simply take the reduced suspension to be the plain suspension equipped with any one of its terms as basepoint (e.g, UFP13, Rem. 8.6.3).

However, in practice it is sometimes convenient to use a different (even if equivalent) construction of the reduced suspension:

Definition

As smash product with the circle type

For a given type $X$, we follow the conventions of the reduced suspension article and write $\mathrm{S} X$ for the plain suspension type of $X$ and $\Sigma X$ for the reduced suspension type of $A$.

The reduced suspension type of a pointed type $(X,x)$ with basepoint term $x \colon X$ may be defined as the smash product type of the pointed circle type $(S^1, s)$ with $X$:

$$\Sigma X \;\coloneqq\; (S^1,s) \wedge (X,x) \,.$$

In cohesive homotopy type theory

In cohesive homotopy type theory, let $(X, x)$ be a pointed cohesive type, and let $\mathbf{\Sigma} X$ be the reduced suspension of $X$, as a cohesive type. Then the reduced suspension type of $X$, as a discrete homotopy type, is the shape of the reduced suspension of $X$: $\Sigma X \coloneqq \esh(\mathbf{\Sigma} X)$.

In particular, if we take $(X, x)$ to be a pointed topological space in real-cohesive homotopy type theory, this allows a construction of reduced suspension types directly from reduced suspensions in classical algebraic topology.

Properties

The reduced suspension type of the $n$-sphere type $S^n$ is equivalent to the $(n + 1)$-sphere type $S^{n + 1}$

$$\Sigma S^n \simeq S^{n + 1}$$

 See also

• suspension object

  • suspension type, reduced suspension type

  • suspension, reduced suspension

References

• Univalent Foundations Project, Rem. 8.6.3 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]