Definition weqsetquotsurj {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X -> Y) (is : issurjective f) (is1 : iscomprelrelfun RX RY f) (is2 : ∏ x x' : X, RY (f x) (f x') -> RX x x') : (setquot RX) ≃ (setquot RY). Proof. intros. set (ff := setquotfun RX RY f is1). split with ff. apply (@isweqinclandsurj (setquotinset RX) (setquotinset RY) ff). apply (isinclsetquotfun RX RY f is1 is2). apply (issurjsetquotfun RX RY f is is1). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.