Lemma setquotbooleqtopaths {X : UU} (R : eqrel X) (is : ∏ x x' : X, isdecprop (R x x')) (x x' : setquot R) : setquotbooleq R is x x' = true -> x = x'. Proof. revert x x'. assert (isp : ∏ (x x' : setquot R), isaprop ((setquotbooleq R is x x') = true -> x = x')). { intros x x'. apply impred. intro. apply (isasetsetquot R x x'). } apply (setquotuniv2prop R (λ x x', make_hProp _ (isp x x'))). simpl. intros x x'. change ((setquotbooleqint R is x x') = true -> paths (setquotpr R x) (setquotpr R x')). unfold setquotbooleqint. induction (pr1 (is x x')) as [ i1 | i2 ]. - intro. apply (weqpathsinsetquot R _ _ i1). - intro H. induction (nopathsfalsetotrue H). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.