{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. Proof. snrapply GraphQuotient_rec. 1: exact (fun x => gq (f x)). intros a b r. apply gqglue. apply e. exact r. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Equivalences. Require Import Types.Universe Types.Paths Types.Arrow Types.Sigma Cubical.DPath.