Spheres (HIT)

Definition

The n-dimensional spheres $S^n$ are higher inductive types defined recursively using the suspension operation and the boolean type.

• $S^0=2$ (the boolean type)
• $S^{n+1}=\Sigma S^n$ (suspension of the n-sphere)

This recursive definition constructs spheres of arbitrary dimension, where each sphere is obtained by suspending the previous one.

Properties

The sphere $S^n$ is the type-theoretic analogue of the topological n-sphere. The definition by iterated suspension ensures that $S^n$ has the expected homotopy type.

The 0-sphere $S^0$ consists of two points with no non-trivial paths between them. The 1-sphere $S^1$ (the circle) has a single point with a non-trivial loop. Higher spheres have increasingly complex homotopy groups.

Related Concepts

Higher Inductive Type Suspension (HIT) Circle (HIT) Boolean Type Homotopy Group Loop Space