Circle (HIT)

Definition

The circle $S^1$ is a Higher Inductive Type with one point and one non-trivial path from that point to itself.

Constructors:

• $\mathrm{base}:S^1$
• $\mathrm{loop}:\mathrm{base}=\mathrm{base}$

The circle is the simplest non-trivial Higher Inductive Type, representing the topological circle as a type with a single basepoint and a loop.

Properties

The circle $S^1$ has fundamental group $\mathbb{Z}$, where loops around the circle correspond to integers via winding number.

Related Concepts

Higher Inductive Type Torus (HIT) Spheres (HIT) Suspension (HIT) Loop Space