Definition isInterval {X:hSet} (S:hsubtype X) (T:WOSubset X) (le : S ⊆ T) : LEM -> sub_initial le -> T ⊈ S -> ∃ t:T, S ≡ upto t. Proof. intros lem ini ne. set (R := WOSrel T). assert (min := WOS_hasSmallest T). set (U := (λ t:T, t ∉ S) : hsubtype (carrier T)). assert (neU : nonempty (carrier U)). { apply (squash_to_hProp ne); intros [x [Tx nSx]]. apply hinhpr. exact ((x,,Tx),,nSx). } clear ne. assert (minU := min U neU); clear min neU. apply (squash_to_hProp minU); clear minU; intros [u [Uu minu]]. apply hinhpr. exists u. intro y. split. - intro Sy. change (∑ Ty : T y, neg (u ≤ y,, Ty)). exists (le y Sy). intro ules. use Uu. exact (ini _ _ _ _ ules). - intro yltu. induction yltu as [yinT yltu]. apply (proof_by_contradiction lem). intro bc. use yltu. now use minu. 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.