proposition: Lemma Torus_rec_beta_loop_b (P : Type) (pb : P) (pla plb : pb = pb) (ps : PathSquare pla pla plb plb) : PathSquare (ap (Torus_rec P pb pla plb ps) loop_b) plb 1 1.
proof: Proof. refine (sq_GGcc _ (eissect _ _) (ds_const'^-1 (Torus_ind_beta_loop_b _ _ _ _ _))). apply moveR_equiv_V, dp_apD_const. Defined.
imports: Basics Cubical