Lemma isinclsetquotfun {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') : isincl (setquotfun RX RY f is1). Proof. intros. apply isinclbetweensets. - apply isasetsetquot. - apply isasetsetquot. - assert (is : ∏ (x x' : setquot RX), isaprop (paths (setquotfun RX RY f is1 x) (setquotfun RX RY f is1 x') -> x = x')). { intros. apply impred. intro. apply isasetsetquot. } apply (setquotuniv2prop RX (λ x x', make_hProp _ (is x x'))). simpl. intros x x'. intro e. set (e' := invweq (weqpathsinsetquot RY (f x) (f x')) e). apply (weqpathsinsetquot RX _ _ (is2 x x' e')). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.