Theorem setquotuniv {X : UU} (R : hrel X) (Y : hSet) (f : X -> Y) (is : iscomprelfun R f) (c : setquot R) : Y. Proof. intros. apply (pr1image (λ x : c, f (pr1 x))). apply (@hinhuniv (pr1 c) (make_hProp _ (isapropimeqclass R Y f is c)) (prtoimage (λ x : c, f (pr1 x)))). apply (eqax0 (pr2 c)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.