Lemma iseqrel_reverse {X : UU} (l : hrel X) : iseqrel l → iseqrel (hrel_reverse l). Proof. intros H. split. now apply ispreorder_reverse, (pr1 H). now apply issymm_reverse, (pr2 H). Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.