{Q : Type} (Qgq : forall a, F a -> Q) (Qgqglue : forall a b (r : R a b) (x : F a), Qgq a x = Qgq b (e _ _ r x)) (a b : A) (s : R a b) (x : F a) : ap (flatten_rec Qgq Qgqglue) (flatten_gqglue s x) = Qgqglue a b s x. Proof. lhs nrapply ap_sig_rec_path_sigma; cbn. lhs nrapply (ap (fun x => x @ _)). { nrapply ap. nrapply (ap01 (fun x => ap10 x _)). nrapply GraphQuotient_ind_beta_gqglue. } apply moveR_pM. apply moveL_pM. do 3 lhs nrapply concat_pp_p. apply moveR_Vp. lhs refine (1 @@ (1 @@ (_ @@ 1))). 1: nrapply (ap10_dpath_arrow DGraphQuotient (fun _ => Q) (gqglue s)). lhs refine (1 @@ (1 @@ _)). { lhs nrapply concat_pp_p. nrapply concat_pp_p. } lhs nrapply (1 @@ concat_V_pp _ _). lhs nrapply concat_V_pp. lhs nrapply concat_pp_p. f_ap. lhs nrapply concat_pp_p. apply moveR_Mp. rhs nrapply concat_Vp. apply moveR_pV. rhs nrapply concat_1p. nrapply ap_V. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.