Theorem weqpathsinsetquot {X : UU} (R : eqrel X) (x x' : X) : R x x' ≃ setquotpr R x = setquotpr R x'. Proof. intros. split with (iscompsetquotpr R x x'). apply isweqimplimpl. - intro e. set (e' := maponpaths (pr1setquot R) e). unfold pr1setquot in e'. unfold setquotpr in e'. simpl in e'. set (e'' := maponpaths (λ f : _, f x') e'). simpl in e''. apply (eqweqmaphProp (pathsinv0 e'') (eqrelrefl R x')). - apply (pr2 (R x x')). - set (int := isasetsetquot R (setquotpr R x) (setquotpr R x')). assumption. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.