Theorem setquotuniv2prop {X : UU} (R : eqrel X) (P : setquot R -> setquot R -> hProp) (is : ∏ x x' : X, P (setquotpr R x) (setquotpr R x')) : ∏ c c' : setquot R, P c c'. Proof. intros. assert (int1 : ∏ c0' : _, P c c0'). { apply (setquotunivprop R (λ c0', P c c0')). intro x. apply (setquotunivprop R (λ c0 : _, P c0 (setquotpr R x))). intro x0. apply (is x0 x). } apply (int1 c'). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.