`{Funext} : Torus <~> Circle * Circle := equiv_adjointify t2c c2t c2t2c t2c2t.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare Require Import Spaces.Circle Spaces.Torus.Torus.