{Q : Type} (Qgq : forall a, F a -> Q) (Qgqglue : forall a b (s : R a b) (x : F a), Qgq a x = Qgq b (e _ _ s x)) : sig DGraphQuotient -> Q. Proof. apply sig_rec. snrapply GraphQuotient_ind. 1: exact Qgq. intros a b s. nrapply dpath_arrow. intros y. lhs nrapply transport_const. lhs nrapply (Qgqglue a b s). f_ap; symmetry. apply transport_DGraphQuotient. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.