proposition: Lemma AC_to_choice_fun (X:hSet) : AxiomOfChoice ⇒ ∥ choice_fun X ∥.
proof: Proof. intros ac. exact (squash_to_hProp (ac (proper_subtypes_set X) (λ S, ∑ x, hProp_to_hSet (¬ (pr1 S x))) pr2) hinhpr). Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets