(x y : A) (s : R x y) (a : F x) (b : F y) : DPath DGraphQuotient (gqglue s) a b <~> (e x y s a = b). Proof. refine (equiv_concat_l _^ _). 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.