`{Funext} : {bl1 : PathSquare (ap (fun y => c2t' base y) loop) loop_b 1 1 & {bl2 : PathSquare (ap (fun x => c2t' x base) loop) loop_a 1 1 & PathCube (sq_ap011 c2t' loop loop) surf bl2 bl2 bl1 bl1}}. Proof. nrefine (_;_;_). unfold sq_ap011. nrefine (cu_concat_lr (cu_ds (dp_apD_nat (fun y => ap_compose _ (fun f => f y) _) _)) _ (sji0:=?[X1]) (sji1:=?X1) (sj0i:=?[Y1]) (sj1i:=?Y1) (pj11:=1)). nrefine (cu_concat_lr (cu_ds (dp_apD_nat (fun x => ap_apply_l _ _ @ apD10 (ap _(Circle_rec_beta_loop _ _ _)) x) _)) _ (sji0:=?[X2]) (sji1:=?X2) (sj0i:=?[Y2]) (sj1i:=?Y2) (pj11:=1)). nrefine (cu_concat_lr (cu_ds (dp_apD_nat (ap10_path_forall _ _ _) _)) _ (sji0:=?[X3]) (sji1:=?X3) (sj0i:=?[Y3]) (sj1i:=?Y3) (pj11:=1)). nrefine (cu_concat_lr (cu_G11 (ap _ (Circle_ind_beta_loop _ _ _))) _ (sji0:=?[X4]) (sji1:=?X4) (sj0i:=?[Y4]) (sj1i:=?Y4) (pj11:=1)). nrefine (cu_concat_lr (cu_G11 (eisretr _ _)) _ (sji0:=?[X5]) (sji1:=?X5) (sj0i:=?[Y5]) (sj1i:=?Y5) (pj11:=1)). apply c2t_square_and_cube.2. Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare Require Import Spaces.Circle Spaces.Torus.Torus.