(P : Type) (pb : P) (pla plb : pb = pb) (ps : PathSquare pla pla plb plb) : PathSquare (ap (Torus_rec P pb pla plb ps) loop_a) pla 1 1. Proof. refine (sq_GGcc _ (eissect _ _) (ds_const'^-1 (Torus_ind_beta_loop_a _ _ _ _ _))). apply moveR_equiv_V, dp_apD_const. Defined.
Require Import Basics.Overture Basics.Equivalences Cubical.DPath