proposition: Lemma equiv_dp_dgraphquotient (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: Proof. refine (equiv_concat_l _^ _). apply transport_DGraphQuotient. Defined.
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences Types.Universe Types.Paths Types.Arrow Types.Sigma Types.Forall Cubical.DPath