fact: Definition DGraphQuotient : GraphQuotient R -> Type := GraphQuotient_rec F (fun x y s => path_universe (e x y s)).
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences Types.Universe Types.Paths Types.Arrow Types.Sigma Types.Forall Cubical.DPath