Lemma weqpathssetquot2l1 {X : UU} (R : eqrel X) (x : X) : iscomprelfun R (λ x', R x x'). Proof. intros. intros x' x''. intro r. apply hPropUnivalence. intro r'. apply (eqreltrans R _ _ _ r' r). intro r''. apply (eqreltrans R _ _ _ r'' (eqrelsymm R _ _ r)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.