{A : Type} (R : Relation A) {sR: is_mere_relation _ R} {B : Type} (S : Relation B) {sS: is_mere_relation _ S} (f : A -> B) (fresp : forall x y, R x y -> S (f x) (f y)) : quotient R -> quotient S. Proof. refine (quotient_rec R (class_of S o f) _). intros x y r. apply related_classes_eq, fresp, r. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.