Theorem weqpathsinsetquot2 {X : UU} (R : eqrel X) (x x' : X) : (R x x') ≃ (setquot2pr R x = setquot2pr R x'). Proof. intros. apply weqimplimpl. apply iscompsetquot2pr. set (int := setquot2univ R hPropset (λ x'', R x x'') (weqpathssetquot2l1 R x)). intro e. change (pr1 (int (setquot2pr R x'))). induction e. change (R x x). apply (eqrelrefl R). apply (pr2 (R x x')). apply (isasetsetquot2). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.