Theorem OrderedSet_univalence (X Y:OrderedSet) : X=Y ≃ X≅Y. Proof. intros. exact ((Poset_univalence _ _) ∘ (underlyingPoset_weq _ _))%weq. 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.