proposition: Lemma isaprop_isPosetEquivalence {X Y : Poset} (f : X ≃ Y) : isaprop (isPosetEquivalence f).
proof: Proof. intros. unfold isPosetEquivalence. apply isapropdirprod; apply isaprop_isaposetmorphism. Defined.
imports: UniMath.Foundations.Propositions