Definition hasSmallest_WOSubset_plus_point {X:hSet} (S:WOSubset X) (z:X) (nSz : ¬ S z) : LEM ⇒ hasSmallest (TOSrel (TOSubset_plus_point S z nSz)). Proof. intros lem T ne. set (S' := TOSubset_plus_point S z nSz). assert (S'z := subtype_plus_has_point S z : S' z). set (z' := (z,,S'z) : carrier S'). set (j := TOSubset_plus_point_incl S z nSz). fold S' in j. set (jmap := subtype_inc j). set (SiT := λ s:S, T (subtype_inc j s)). induction (lem (∃ s, SiT s)) as [q|q]. - assert (SiTmin := WOS_hasSmallest _ _ q). apply (squash_to_hProp SiTmin); clear SiTmin; intros [m [SiTm min]]. apply hinhpr. set (m' := jmap m). exists m'. split. + exact SiTm. + intros [t S't] Tt. apply (squash_to_hProp S't); intros [St|etz]. * induction (ishinh_irrel (ii1 St) S't); change (m ≤ (t,,St)). exact (min (t,,St) Tt). * induction etz; induction (ishinh_irrel (ii2 (idpath z)) S't); change unit. exact tt. - apply hinhpr. exists z'. split. + apply (squash_to_hProp ne); clear ne; intros [[t SiTt] Tt]. apply (squash_to_hProp SiTt); intros [St|ezt]. * apply fromempty. apply q. apply hinhpr. exists (t,,St). change (T (t,, j t St)). induction (proofirrelevance_hProp _ SiTt (j t St)). exact Tt. * induction ezt. unfold z'. induction (proofirrelevance_hProp _ SiTt S'z). exact Tt. + intros [t S't] Tt. apply (squash_to_hProp S't); intros [St|ezt]. * apply fromempty. apply q; clear q. apply hinhpr. exists (t,,St). change (T (t,, j t St)). induction (proofirrelevance_hProp _ S't (j t St)). exact Tt. * induction ezt. change (TOSrel S' (z,,S'z) (z,,S't)). induction (proofirrelevance_hProp _ S'z S't). exact (TOrefl S' _). 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.