Homotopy Type Theory
spheres (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed


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.


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

S n:=Σ nS 0S^n := \Sigma^n S^0


See also


Revision on February 14, 2019 at 15:19:40 by Mike Shulman. See the history of this page for a list of all contributions to it.