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