Lemma isantisymmnegtoiscoantisymm {X : UU} {R : hrel X} (isdr : isdecrel R) (isr : isantisymmneg R) : iscoantisymm R. Proof. intros. intros x1 x2 nrx12. induction (isdr x2 x1) as [ r | nr ]. apply (ii1 r). apply ii2. apply (isr _ _ nrx12 nr). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.