Lemma wosub_le_isPartialOrder X : isPartialOrder (wosub_le X). Proof. repeat split. - intros S T U i j. exists (pr11 (subtype_containment_isPartialOrder X) S T U (pr1 i) (pr1 j)). split. + intros s s' l. exact (wosub_le_comp j _ _ (wosub_le_comp i _ _ l)). + intros s u Ss Uu l. change (hProptoType ((u,,Uu) ≤ subtype_inc (pr1 j) (subtype_inc (pr1 i) (s,,Ss)))) in l. set (uinT := u ,, wosub_le_subi j s u (pr1 i s Ss) Uu l : T). assert (p : subtype_inc (pr1 j) uinT = u,,Uu). { now apply subtypePath_prop. } assert (q := h1 p l : subtype_inc (pr1 j) uinT ≤ subtype_inc (pr1 j) (subtype_inc (pr1 i) (s,,Ss))). assert (r := pr2 (wosub_fidelity j _ _) q). assert (b := wosub_le_subi i _ _ _ _ r); simpl in b. exact b. - apply wosub_le_isrefl. - intros S T i j. apply (invmap (wosub_univalence _ _)). exact (i,,j). 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.