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