Theorem isdeceqsetquot_non_constr {X : UU} (R : eqrel X) (is : ∏ x x' : X, isdecprop (R x x')) : isdeceq (setquot R). Proof. intros. apply isdeceqif. intros x x'. apply (setquotuniv2prop R (λ x0 x0', make_hProp _ (isapropisdecprop (x0 = x0')))). intros x0 x0'. simpl. apply (isdecpropweqf (weqpathsinsetquot R x0 x0') (is x0 x0')). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.