Definition eqrel_reverse {X : UU} (l : eqrel X) := make_eqrel (hrel_reverse l) (iseqrel_reverse l (pr2 l)).
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.