{s : PathSquare loop_a loop_a (ap (Circle_rec _ tbase loop_b) loop) (ap (Circle_rec _ tbase loop_b) loop) & PathCube s surf hr hr (sq_G1 (Circle_rec_beta_loop _ _ _)) (sq_G1 (Circle_rec_beta_loop _ _ _))}. Proof. apply cu_fill_left. Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare Require Import Spaces.Circle Spaces.Torus.Torus.