`{Funext} : t2c o c2t == idmap. Proof. nrapply prod_ind. snrefine (Circle_ind _ (Circle_ind _ 1 _) _). 1: apply sq_dp^-1, sq_tr^-1; shelve. apply dp_forall_domain. intro x; apply sq_dp^-1; revert x. snrefine (Circle_ind _ _ _). 1: apply sq_tr^-1; shelve. apply dp_cu. nrefine (cu_ccGGcc _ _ _). 1,2: nrefine (ap sq_dp (Circle_ind_beta_loop _ _ _) @ eisretr _ _)^. apply cu_rot_tb_fb. nrefine (cu_ccGGGG _ _ _ _ _). 1,2,3,4: exact (eisretr _ _)^. nrefine ((sq_ap011_compose c2t' t2c loop loop) @lr (cu_ap t2c (c2t'_beta.2.2)) @lr (Torus_rec_beta_surf _ _ _ _ _) @lr (cu_flip_lr (sq_ap_idmap _)) @lr (sq_ap_uncurry _ _ _)). Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare Require Import Spaces.Circle Spaces.Torus.Torus.