open import 1Lab.Univalence open import 1Lab.HIT.S1 open import 1Lab.Equiv open import 1Lab.Path open import 1Lab.Type module 1Lab.HIT.Torus where
The Torus🔗
In classical topology, the two-dimensional torus may be defined as the product of circles, i.e., may be defined as . Alternatively, the space may be presented as a CW complex, built by beginning with a point, attaching two 1-cells to form the wedge of two circles, and finishing by attaching a 2-cell.
Such a CW complex can be regarded as a higher inductive type, regarding the 0-cell as a constructor base, the two 1-cells as distinct paths base ≡ base, and the 2-cell as a square with its top and bottom edges attached to one of the 1-cells, and its left and right edge attachd to the other.
data T² : Type where base : T² loopA : base ≡ base loopB : base ≡ base square : Square loopA loopB loopB loopA
The resulting HIT is equivalent to the product of two circles.
open is-iso T²≃S¹×S¹ : T² ≡ ( S¹ × S¹ ) T²≃S¹×S¹ = ua (T²→S¹×S¹ , is-iso→is-equiv iso-pf) where T²→S¹×S¹ : T² → S¹ × S¹ T²→S¹×S¹ base = base , base T²→S¹×S¹ (loopA i) = loop i , base T²→S¹×S¹ (loopB j) = base , loop j T²→S¹×S¹ (square i j) = loop i , loop j S¹×S¹→T² : S¹ × S¹ → T² S¹×S¹→T² (base , base) = base S¹×S¹→T² (base , loop j) = loopB j S¹×S¹→T² (loop i , base) = loopA i S¹×S¹→T² (loop i , loop j) = square i j iso-pf : is-iso T²→S¹×S¹ iso-pf .inv = S¹×S¹→T² iso-pf .rinv (base , base) = refl iso-pf .rinv (base , loop j) = refl iso-pf .rinv (loop i , base) = refl iso-pf .rinv (loop i , loop j) = refl iso-pf .linv base = refl iso-pf .linv (loopA i) = refl iso-pf .linv (loopB j) = refl iso-pf .linv (square i j) = refl
Showing that the torus described as a HIT is equivalent to the product of two circles is Exercise 6.3 of the HoTT Book, but this exercise includes a warning that “the path algebra for this is rather difficult.” The brevity of the above proof – straightforward invocations of refl – is a testament to the strength of cubical methods.