Definition setquotuniv2 {X : UU} (R : hrel X) (Y : hSet) (f : X -> X -> Y) (is : iscomprelfun2 R f) (c c0 : setquot R) : Y. Proof. intros. set (ff := λ xy : dirprod X X, f (pr1 xy) (pr2 xy)). set (RR := hreldirprod R R). apply (setquotuniv RR Y ff (setquotuniv2_iscomprelfun R Y f is c c0) (dirprodtosetquot R R (make_dirprod c c0))). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.