Definition isdeceqsetquot {X : UU} (R : eqrel X) (is : ∏ x x' : X, isdecprop (R x x')) : isdeceq (setquot R). Proof. intros. intros x x'. induction (boolchoice (setquotbooleq R is x x')) as [ i | ni ]. - apply (ii1 (setquotbooleqtopaths R is x x' i)). - apply ii2. intro e. induction (falsetonegtrue _ ni (setquotpathstobooleq R is x x' e)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.