Lemma isapropimeqclass {X : UU} (R : hrel X) (Y : hSet) (f : X -> Y) (is : iscomprelfun R f) (c : setquot R) : isaprop (image (λ x : c, f (pr1 x))). Proof. intros. apply isapropsubtype. intros y1 y2. simpl. apply (@hinhuniv2 _ _ (make_hProp (y1 = y2) (pr2 Y y1 y2))). intros x1 x2. simpl. induction c as [ A iseq ]. induction x1 as [ x1 is1 ]. induction x2 as [ x2 is2 ]. induction x1 as [ x1 is1' ]. induction x2 as [ x2 is2' ]. simpl in is1. simpl in is2. simpl in is1'. simpl in is2'. assert (r : R x1 x2) by apply (eqax2 iseq _ _ is1' is2'). apply (pathscomp0 (pathsinv0 is1) (pathscomp0 (is _ _ r) is2)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.