Definition isantisymmlogeqf {X : UU} {L R : hrel X} (lg : ∏ x1 x2, L x1 x2 <-> R x1 x2) (isl : isantisymm L) : isantisymm R. Proof. intros. intros x1 x2 r12 r21. apply (isl _ _ (pr2 (lg _ _) r12) (pr2 (lg _ _) r21)). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.