proposition: Lemma functor_gq_idmap {A : Type} {R : A -> A -> Type} : functor_gq (A:=A) (B:=A) (S:=R) idmap (fun a b r => r) == idmap.
proof: 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.
imports: Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences Types.Universe Types.Paths Types.Arrow Types.Sigma Types.Forall Cubical.DPath