Lemma iscomprelrelfun_eqrel_from_hrel (X X' : UU) (R : hrel X) (R' : hrel X') (f : X → X') (Hf : iscomprelrelfun R R' f) : iscomprelrelfun (eqrel_from_hrel R) (eqrel_from_hrel R') f. Proof. intros x x' Hx. intros R0 HR0. apply (Hx (mapeqrel f R0)). intros y y' Hy. apply HR0. apply Hf. apply Hy. Qed.