Definition transportFiniteOrdering {n} {X:UU} : X ≃ ⟦ n ⟧ -> FiniteOrderedSet. Proof. intros w. simple refine (_,,_). - simple refine (_,,_). * simple refine (_,,_). + exists X. apply (isofhlevelweqb 2 w). apply setproperty. + unfold PartialOrder; simpl. simple refine (_,,_). { intros x y. exact (w x ≤ w y). } apply inducedPartialOrder_weq. exact (pr2 (pr2 (pr1 (pr1 (⟦ n ⟧))))). * intros x y. apply (pr2 (pr1 (⟦ n ⟧))). - simpl. apply (isfiniteweqb w). exact (pr2 (⟦ n ⟧)). 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.