{x} : F x -> sig DGraphQuotient. Proof. intros p. exact (gq x; p). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.