`{Funext} : c2t o t2c == idmap. Proof. nrefine (Torus_ind _ 1 _ _ _). apply cu_ds^-1. refine (cu_GGGGcc (eisretr _ _)^ (eisretr _ _)^ (eisretr _ _)^ (eisretr _ _)^ _). apply cu_rot_tb_fb. refine (cu_ccGGGG (eisretr _ _)^ (eisretr _ _)^ (eisretr _ _)^ (eisretr _ _)^ _). nrefine ((sq_ap_compose t2c c2t surf) @lr (cu_ap c2t (Torus_rec_beta_surf _ _ _ _ _ )) @lr (sq_ap_uncurry _ _ _) @lr (pr2 (pr2 c2t'_beta)) @lr (cu_flip_lr (sq_ap_idmap _))). Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare Require Import Spaces.Circle Spaces.Torus.Torus.