Lemma mapeqrel_iseqrel {X X' : UU} (f : X → X') (R : eqrel X') : iseqrel (maphrel f R). Proof. repeat split. - intros x x' x''. apply eqreltrans. - intro x. apply eqrelrefl. - intros x y. apply eqrelsymm. Qed.