Definition theSmallest {X : WellOrderedSet} (S : hsubtype X) : hProp := (∃ s, S s) ⇒ make_hProp (∑ s:X, S s ∧ ∀ t:X, S t ⇒ WOrel X s t)%type (isaprop_theSmallest _ (WO_isTotalOrder X) 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.