Lemma istrans_reverse {X : UU} (l : hrel X) : istrans l → istrans (hrel_reverse l). Proof. intros Hl x y z Hxy Hyz. now apply (Hl z y x). Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.