Homotopy Type Theory spheres > history (Rev #2)

Idea

Spheres can be thought of as a space generated by a point and a (higher-)path constructor. This does not mean their homotopical information is simple however. In face it is very much still an open problem to determine the homotopy groups of spheres.

Definition

The $n$-sphere can be defined as the suspension of the $(n-1)$-sphere or the iterated suspension of $S^0 := \mathbf{2}$. (a.k.a $\text{Bool}$).

Properties

See also

• homotopy groups of spheres
• Synthetic homotopy theory

References

• HoTT book