Definition is_guided_WOSubset {X:hSet} (g : choice_fun X) (C : WOSubset X) : hProp := ∀ c:C, pr1 c = pr1 (g (upto' c)).
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.