`{Funext} : Circle * Circle -> Torus. Proof. apply uncurry, '. Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare Require Import Spaces.Circle Spaces.Torus.Torus.