Lemma iscompsetquot2pr {X : UU} (R : hrel X) : iscomprelfun R (setquot2pr R). Proof. intros. intros x x' r. assert (e1: paths (compevmapset R x) (compevmapset R x')). { apply funextsec. intro S. apply funextsec. intro f. unfold compfun in f. apply (pr2 f x x' r). } apply (invmaponpathsincl _ (isinclpr1image (compevmapset R)) (setquot2pr R x) (setquot2pr R x') e1). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.