Lemma setquotpathstobooleq {X : UU} (R : eqrel X) (is : ∏ x x' : X, isdecprop (R x x')) (x x' : setquot R) : x = x' -> setquotbooleq R is x x' = true. Proof. intros e. induction e. generalize x. apply (setquotunivprop R (λ x, make_hProp _ (isasetbool (setquotbooleq R is x x) true))). simpl. intro x0. change ((setquotbooleqint R is x0 x0) = true). unfold setquotbooleqint. induction (pr1 (is x0 x0)) as [ i1 | i2 ]. - apply idpath. - induction (i2 (eqrelrefl R x0)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.