Lemma isaprop_theSmallest {X : hSet} (R : hrel X) (total : isTotalOrder R) (S : hsubtype X) : isaprop (∑ s:X, hProp_to_hSet (S s ∧ ∀ t:X, S t ⇒ R s t)). Proof. induction total as [[po anti] tot]. apply invproofirrelevance; intros s t. apply subtypePath_prop. induction s as [x i], t as [y j], i as [I i], j as [J j]. change (x=y)%logic. apply (squash_to_hProp (tot x y)); intros [c|c]. { apply anti. { exact c. } { exact (j x I). } } { apply anti. { exact (i y J). } { exact c. } } 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.