{A B : Type} (f : A <~> B) (R : A -> A -> Type) (S : B -> B -> Type) (e : forall a b, R a b <~> S (f a) (f b)) : GraphQuotient R <~> GraphQuotient S := Build_Equiv _ _ (functor_gq f e) _.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.