Definition WosubPoset (X:hSet) : Poset. Proof. exists (WOSubset_set X). exists (λ S T, S ≼ T). exact (wosub_le_isPartialOrder X). Defined.
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.