Lemma wosub_fidelity {X:hSet} {S T:WOSubset X} (le : S ≼ T) (s s' : S) : s ≤ s' ⇔ wosub_inc le s ≤ wosub_inc le s'. Proof. set (Srel := WOSrel S). assert (Stot : istotal Srel). { apply (WOSwo S). } set (Trel := WOSrel T). assert (Tanti : isantisymm Trel). { apply (WOSwo T). } split. { intro l. exact (wosub_le_comp le s s' l). } { intro l. apply (squash_to_hProp (Stot s s')). change ((s ≤ s') ⨿ (s' ≤ s) → s ≤ s'). intro c. induction c as [c|c]. - exact c. - induction le as [le [com ini]]. assert (k := com s' s c). assert (k' := Tanti _ _ l k); clear k. assert (p : s = s'). { apply subtypePath_prop. exact (maponpaths pr1 k'). } induction p. apply (pr2 S). } 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.