Theorem Poset_univalence (X Y:Poset) : X=Y ≃ X≅Y. Proof. intros. assert (k : pr1weq (Poset_univalence_0 X Y) ~ @Poset_univalence_map X Y). { intro e. apply isinj_pr1_PosetEquivalence. induction e. reflexivity. } exact (remakeweq k). 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.