Torus -> Circle * Circle. Proof. snrapply Torus_rec. + exact (base, base). + exact (path_prod' loop 1). + exact (path_prod' 1 loop). + exact (sq_prod (hr, vr)). Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare Require Import Spaces.Circle Spaces.Torus.Torus.