Definition setquotfun2 {X Y : UU} (RX : hrel X) (RY : eqrel Y) (f : X -> X -> Y) (is : iscomprelrelfun2 RX RY f) (cx cx0 : setquot RX) : setquot RY. Proof. intros. set (ff := λ x x0 : X, setquotpr RY (f x x0)). exact (setquotuniv2 RX (setquotinset RY) ff (setquotfun2_iscomprelfun2 RX RY f is cx cx0) cx cx0). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.