Lemma issurjsetquotfun {X Y : UU} (RX : eqrel X) (RY : eqrel Y) (f : X -> Y) (is : issurjective f) (is1 : iscomprelrelfun RX RY f) : issurjective (setquotfun RX RY f is1). Proof. intros. apply (issurjtwooutof3b (setquotpr RX)). apply (issurjcomp f (setquotpr RY) is (issurjsetquotpr RY)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.