Lemma isinj_pr1_PosetEquivalence (X Y : Poset) : isInjective (pr1 : X ≅ Y -> X ≃ Y). Proof. intros f g. apply isweqonpathsincl. apply isincl_pr1_PosetEquivalence. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.