Definition setquotincl {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X -> Y) (is1 : iscomprelrelfun RX RY f) (is2 : ∏ x x' : X, RY (f x) (f x') -> RX x x') : incl (setquot RX) (setquot RY) := make_incl (setquotfun RX RY f is1) (isinclsetquotfun RX RY f is1 is2).
Require Import UniMath.Foundations.UnivalenceAxiom.