proposition: Lemma mapeqrel_iseqrel {X X' : UU} (f : X → X') (R : eqrel X') : iseqrel (maphrel f R).
proof: Proof. repeat split. - intros x x' x''. apply eqreltrans. - intro x. apply eqrelrefl. - intros x y. apply eqrelsymm. Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.Foundations.Sets