proposition: Theorem OrderedSet_univalence (X Y:OrderedSet) : X=Y ≃ X≅Y.
proof: Proof. intros. exact ((Poset_univalence _ _) ∘ (underlyingPoset_weq _ _))%weq. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions