fact: Definition WOSubset_to_TOSubset {X:hSet} : WOSubset X -> TOSubset X := λ S, WOSubset_to_subtype S,, WOSrel S,, WOStotal S.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets