Torus (HIT)

Definition

The torus $T^2$ is a Higher Inductive Type with a 2-dimensional path constructor, representing the topological torus.

Constructors:

• $b:T^2$ (basepoint)
• $p:b=b$ (first loop)
• $q:b=b$ (second loop)
• $s:p\cdot q=q\cdot p$ (surface witnessing commutativity)

The torus is defined natively as a HIT with a basepoint, two loops through that point, and a 2-dimensional path (surface) witnessing that the two loops commute.

Properties

The torus $T^2$ has fundamental group $\mathbb{Z}\times \mathbb{Z}$, corresponding to the two independent loops $p$ and $q$.

The 2-dimensional path constructor $s$ ensures that the two loops commute up to homotopy, which is essential for the correct homotopy type of the torus.

Alternative Definitions

The torus can also be defined as the product $S^1\times S^1$ of two circles, which is provably equivalent to this HIT definition.

Related Concepts

Higher Inductive Type Circle (HIT) Spheres (HIT) Product Type Fundamental Group Homotopy Group