{A : Type} (R : Relation A) {B : Type} (S : Relation B) (f : A -> B) (fresp : forall a b, R a b -> S (f a) (f b)) : Quotient R -> Quotient S. Proof. refine (Quotient_rec R _ (class_of S o f) _). intros a b p. apply qglue, fresp, p. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.