{A : Type} {R : A -> A -> Type} : functor_gq (A:=A) (B:=A) (S:=R) idmap (fun a b r => r) == idmap. Proof. snrapply GraphQuotient_ind. 1: reflexivity. intros a b r. nrapply (transport_paths_FlFr' (gqglue r)). apply equiv_p1_1q. rhs nrapply ap_idmap. nrapply GraphQuotient_rec_beta_gqglue. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.