Lemma isaprop_isantisymm {X : hSet} (R : hrel X) : isaprop (isantisymm R). Proof. intros. unfold isantisymm. apply impred; intro x. apply impred; intro y. apply impred; intro r. apply impred; intro s. apply setproperty. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.