proposition: 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: 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.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets