{x y} (s : R x y) (a : F x) : transport DGraphQuotient (gqglue s) a = e x y s a. Proof. lhs nrapply transport_idmap_ap. lhs nrapply (transport2 idmap). 1: apply GraphQuotient_rec_beta_gqglue. rapply transport_path_universe. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.