Lemma isaprop_isPosetEquivalence {X Y : Poset} (f : X ≃ Y) : isaprop (isPosetEquivalence f). Proof. intros. unfold isPosetEquivalence. apply isapropdirprod; apply isaprop_isaposetmorphism. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.