Theorem setquotunivprop {X : UU} (R : eqrel X) (P : setquot (pr1 R) -> hProp) (ps : ∏ x : X, pr1 (P (setquotpr R x))) : ∏ c : setquot (pr1 R), pr1 (P c). Proof. intros c. apply (@hinhuniv (carrier (pr1 c)) (P c)). - intro x. set (e := setquotl0 R c x). apply (eqweqmaphProp (maponpaths P e)). exact (ps (pr1 x)). - exact (eqax0 (pr2 c)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.