Definition quotdecrelintlogeq {X : UU} {R : eqrel X} (L : decrel X) (is : iscomprelrel R (pr1 L)) (x x' : setquot R) : breltodecrel (quotdecrelint L is) x x' <-> quotrel is x x'. Proof. revert x x'. assert (int : ∏ (x x' : setquot R), isaprop ((quotdecrelint L is x x') = true <-> (quotrel is x x'))). { intros x x'. apply isapropdirprod. - apply impred. intro. apply (pr2 (quotrel _ _ _)). - apply impred. intro. apply isasetbool. } apply (setquotuniv2prop R (λ x x', make_hProp _ (int x x'))). intros x x'. simpl. split. - apply (pathstor L x x'). - apply (rtopaths L x x'). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.