Lemma iscompsetquotpr {X : UU} (R : eqrel X) (x x' : X) (a : R x x') : setquotpr R x = setquotpr R x'. Proof. intros. apply (invmaponpathsincl _ (isinclpr1setquot R)). simpl. apply funextsec. intro x0. apply hPropUnivalence. intro r0. apply (eqreltrans R _ _ _ (eqrelsymm R _ _ a) r0). intro x0'. apply (eqreltrans R _ _ _ a x0'). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.