Lemma iscoasymmgenrel {X : UU} (R : hrel X) (isr : isasymm R) : iscoasymm (negrel R). Proof. intros. intros x1 x2 nr12. apply (negf (isr _ _) nr12). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.