Lemma istransnegrel {X : UU} (R : hrel X) (isr : iscotrans R) : istrans (negrel R). Proof. intros. intros x1 x2 x3 r12 r23. apply (negf (isr x1 x2 x3)). apply (toneghdisj (make_dirprod r12 r23)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.