Definition isPosetEquivalence_idweq (X : Poset) : isPosetEquivalence (idweq X). Proof. intros. split. - intros x y le. exact le. - intros x y le. exact le. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.