Definition WOSubset_to_TOSubset {X:hSet} : WOSubset X -> TOSubset X := λ S, WOSubset_to_subtype S,, WOSrel S,, WOStotal S.
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.