c2t' `{Funext} : Circle -> Circle -> Torus. Proof. snrapply Circle_rec. + snrapply Circle_rec. - exact tbase. - exact loop_b. + apply path_forall. snrapply Circle_ind. - exact loop_a. - srapply sq_dp^-1. apply (pr1 c2t_square_and_cube). Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare Require Import Spaces.Circle Spaces.Torus.Torus.