Lemma iscotrans_reverse {X : UU} (l : hrel X) : iscotrans l -> iscotrans (hrel_reverse l). Proof. intros Hl x y z H. now apply islogeqcommhdisj, Hl. Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.