Definition setquotfun {X Y : UU} (RX : hrel X) (RY : eqrel Y) (f : X -> Y) (is : iscomprelrelfun RX RY f) (cx : setquot RX) : setquot RY. Proof. intros. set (ff := funcomp f (setquotpr RY)). assert (isff : iscomprelfun RX ff). { intros x x'. intro r. apply (weqpathsinsetquot RY (f x) (f x')). apply is. apply r. } apply (setquotuniv RX (setquotinset RY) ff isff cx). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.