Lemma isincl_pr1_PosetEquivalence (X Y : Poset) : isincl (pr1 : X ≅ Y -> X ≃ Y). Proof. intros. apply isinclpr1. apply isaprop_isPosetEquivalence. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.