Definition Poset_univalence_map {X Y:Poset} : X=Y -> PosetEquivalence X Y. Proof. intros e. induction e. apply identityPosetEquivalence. Defined.
Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.OrderTheory.Posets.Examples.StandardFiniteSet.