proposition: 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: Proof. intros x x' Hx. intros R0 HR0. apply (Hx (mapeqrel f R0)). intros y y' Hy. apply HR0. apply Hf. apply Hy. Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.Foundations.Sets