Definition iscoantisymmlogeqf {X : UU} {L R : hrel X} (lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : iscoantisymm L) : iscoantisymm R. Proof. intros. intros x1 x2 r12. set (int := isl _ _ (negf (pr1 (lg _ _)) r12)). generalize int. clear int. simpl. apply (coprodf (pr1 (lg _ _)) (idfun _)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.