Lemma tosub_fidelity {X:hSet} {S T:TOSubset X} (le : S ≼ T) (s s' : S) : s ≤ s' ⇔ subtype_inc (pr1 le) s ≤ subtype_inc (pr1 le) s'. Proof. split. { exact (pr2 le s s'). } { intro l. apply (squash_to_hProp (TOtot S s s')). intros [c|c]. - exact c. - apply (TOeq_to_refl S s s'). assert (k := pr2 le _ _ c); clear c. assert (k' := TOanti T _ _ l k); clear k l. apply subtypePath_prop. exact (maponpaths pr1 k'). } 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.