Definition setquotuniv2' {X Y} (RX:hrel X) (RY:hrel Y) {Z:hSet} (f:X->Y->Z) (is:iscomprelfun2' RX RY f) : setquot RX -> setquot RY -> Z. Proof. intros x''. simple refine (setquotuniv RX (funset (setquot RY) Z) _ _ _). { simpl. intro x. apply (setquotuniv RY Z (f x)). intros y y' e. unfold iscomprelfun2 in is. apply (pr2 is). assumption. } { intros x x' e. assert( p : f x = f x' ). { apply funextsec; intro y. apply (pr1 is). assumption. } apply setquotuniv_equal. assumption. } assumption. Defined.
Require Import