{Q : sig DGraphQuotient -> Type} (Qgq : forall a (x : F a), Q (flatten_gq x)) (Qgqglue : forall a b (s : R a b) (x : F a), flatten_gqglue s x # Qgq _ x = Qgq _ (e _ _ _ x)) : forall x, Q x. Proof. apply sig_ind. snrapply GraphQuotient_ind. 1: exact Qgq. intros a b s. apply dp_forall. intros x y. srapply (equiv_ind (equiv_dp_dgraphquotient a b s x y)^-1). intros q. destruct q. refine (transport2 _ _ _ @ Qgqglue a b s x). refine (ap (path_sigma_uncurried DGraphQuotient _ _) _). snrapply path_sigma. 1: reflexivity. lhs nrapply concat_p1. apply inv_V. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.