Definition underlyingPoset_weq (X Y:OrderedSet) : X=Y ≃ (underlyingPoset X)=(underlyingPoset Y). Proof. Set Printing Coercions. intros. simple refine (make_weq _ _). { apply maponpaths. } apply isweqonpathsincl. apply isincl_underlyingPoset. Unset Printing Coercions. 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.