Lemma guided_WOSubset_total {X:hSet} (g : choice_fun X) : LEM -> is_wosubset_chain (guidedFamily g). Proof. intros lem [C gC] [D gD]. set (W := max_common_initial C D). assert (Q := max_common_initial_is_common_initial C D). induction Q as [WC [WD [WCi [WDi WCD]]]]; fold W in WC, WD, WCi, WDi. assert (E : W ≡ C ∨ W ≡ D). { apply (proof_by_contradiction lem); intro h. assert (k := fromnegcoprod_prop h); clear h; induction k as [nc nd]. assert (nCW : C ⊈ W). { use subtype_notEqual_containedIn. - exact WC. - now apply subtype_notEqual_from_negEqual. } assert (nDW : D ⊈ W). { use subtype_notEqual_containedIn. - exact WD. - now apply subtype_notEqual_from_negEqual. } assert (p : ∃ t : C, W ≡ upto t). { now use isInterval. } assert (q : ∃ t : D, W ≡ upto t). { now use isInterval. } change hfalse. apply (squash_to_hProp p); clear p; intros [c cE]. apply (squash_to_hProp q); clear q; intros [d dE]. assert (ce : W = upto c). { now apply (invmap (hsubtype_univalence _ _)). } assert (de : W = upto d). { now apply (invmap (hsubtype_univalence _ _)). } assert (cd := !ce @ de : upto c = upto d). assert (cd' : upto' c = upto' d). { now apply subtypePath_prop. } assert (p := gC c); simpl in p. assert (q := gD d); simpl in q. unfold choice_fun in g. assert (cd1 : pr1 c = pr1 d). { simple refine (p @ _ @ !q). now induction cd'. } clear cd'. set (W' := subtype_plus W (pr1 c)). assert (j := subtype_plus_incl W (pr1 c) : W ⊆ W'). assert (W'c := subtype_plus_has_point W (pr1 c) : W' (pr1 c)). assert (W'd := transportf W' cd1 W'c : W' (pr1 d)). assert (ci : common_initial W' C D). { assert (W'C := subtype_plus_in WC (pr2 c)); assert (W'D := subtype_plus_in WD (transportb (λ x : X, D x) cd1 (pr2 d))); fold W' in W'C, W'D. exists W'C, W'D. assert (cmax : ∏ (v : carrier W') (W'c : W' (pr1 c)), subtype_inc W'C v ≤ subtype_inc W'C (pr1 c,,W'c)). { intros v W'c'. assert (e : c = subtype_inc W'C (pr1 c,, W'c')). { now apply subtypePath_prop. } induction e. clear W'c'. induction v as [v W'v]. apply (squash_to_hProp W'v); intros [Wv|k]. - assert (L := pr1 (cE v) Wv). unfold upto,lt in L. assert (Q := @tot_nge_to_le (carrier_subset C) (TOSrel C) (TOtot C) _ _ (pr2 L)). now apply(h1'' Q). - use (TOeq_to_refl C). apply subtypePath_prop. simpl. exact (!k). } assert (cmax' : ∏ (w : carrier W) (W'c : W' (pr1 c)), subtype_inc W'C (subtype_inc j w) < subtype_inc W'C (pr1 c,,W'c)). { intros w W'c'. assert (e : c = subtype_inc W'C (pr1 c,, W'c')). { now apply subtypePath_prop. } induction e. clear W'c'. induction w as [v Wv]. assert (L := pr1 (cE v) Wv). unfold upto,lt in L. assert (Q := @tot_nge_to_le (carrier_subset C) (TOSrel C) (TOtot C) _ _ (pr2 L)). apply (@tot_nle_iff_gt (carrier_subset C) (TOSrel C) (pr122 C)). split. - now apply (h1'' Q). - intros e. assert (e' := maponpaths pr1 e); clear e. change (v = pr1 c)%type in e'. assert ( L' := pr2 L ). simpl in L'. apply L'; clear L'. exact (TOeq_to_refl_1 C c (v,, pr1 L) (!e')). } assert (dmax : ∏ (v : carrier W') (W'd : W' (pr1 d)), subtype_inc W'D v ≤ subtype_inc W'D (pr1 d,,W'd)). { intros v W'd'. assert (e : d = subtype_inc W'D (pr1 d,, W'd')). { now apply subtypePath_prop. } induction e. clear W'd'. induction v as [v W'v]. apply (squash_to_hProp W'v); intros [Wv|k]. - assert (L := pr1 (dE v) Wv). unfold upto,lt in L. assert (Q := @tot_nge_to_le (carrier_subset D) (TOSrel D) (TOtot D) _ _ (pr2 L)). now apply(h1'' Q). - use (TOeq_to_refl D). apply subtypePath_prop. simpl. exact (!k @ cd1). } assert (dmax' : ∏ (w : carrier W) (W'd : W' (pr1 d)), subtype_inc W'D (subtype_inc j w) < subtype_inc W'D (pr1 d,,W'd)). { intros w W'd'. assert (e : d = subtype_inc W'D (pr1 d,, W'd')). { now apply subtypePath_prop. } induction e. clear W'd'. induction w as [v Wv]. assert (L := pr1 (dE v) Wv). unfold upto,lt in L. assert (Q := @tot_nge_to_le (carrier_subset D) (TOSrel D) (TOtot D) _ _ (pr2 L)). apply (@tot_nle_iff_gt (carrier_subset D) (TOSrel D) (pr122 D)). split. - now apply (h1'' Q). - intros e. assert (e' := maponpaths pr1 e); clear e. change (v = pr1 d)%type in e'. assert ( L' := pr2 L ). simpl in L'. apply L'; clear L'. exact (TOeq_to_refl_1 D d (v,, pr1 L) (!e')). } split. { intros w' c' W'w' Cc' le. apply (squash_to_hProp W'w'); intros B. induction B as [Ww'|e]. - apply hinhpr, ii1. apply (WCi w' c' Ww' Cc'). now apply (h1'' le). - induction e. induction (lem (pr1 c = c')) as [e|ne]. + induction e. exact W'c. + use j. rewrite ce. exists Cc'. unfold lt. intro le'. apply ne. assert (e : c = (c',,Cc')). { apply (TOanti C). - exact le'. - now apply (h1'' le). } exact (maponpaths pr1 e). } split. { intros w' d' W'w' Dd' le. apply (squash_to_hProp W'w'); intros B. induction B as [Ww'|e]. - apply hinhpr, ii1. apply (WDi w' d' Ww' Dd'). now apply (h1'' le). - induction e. induction (lem (pr1 d = d')) as [e|ne]. + induction e. exact W'd. + use j. rewrite de. exists Dd'. unfold lt. intro le'. apply ne. assert (e : d = (d',,Dd')). { apply (TOanti D). - exact le'. - now apply (h1'' le). } exact (maponpaths pr1 e). } { intros [v W'v] [w W'w]. change (hProptoType (W' v)) in W'v; change (hProptoType (W' w)) in W'w. apply (squash_to_hProp W'v); intros [Wv|Ev]. - apply (squash_to_hProp W'w); intros [Ww|Ew]. + assert (Q := WCD (v,,Wv) (w,,Ww)). change (hProptoType ( (subtype_inc WC (v,, Wv) ≤ subtype_inc WC (w,, Ww)) ⇔ (subtype_inc WD (v,, Wv) ≤ subtype_inc WD (w,, Ww)) )%tosubset) in Q. assert (e : subtype_inc W'C (v,, W'v) = subtype_inc WC (v,, Wv)). { now apply subtypePath_prop. } induction e. assert (e : subtype_inc W'C (w,, W'w) = subtype_inc WC (w,, Ww)). { now apply subtypePath_prop. } induction e. assert (e : subtype_inc W'D (v,, W'v) = subtype_inc WD (v,, Wv)). { now apply subtypePath_prop. } induction e. assert (e : subtype_inc W'D (w,, W'w) = subtype_inc WD (w,, Ww)). { now apply subtypePath_prop. } induction e. exact Q. + induction Ew. apply logeq_if_both_true. * apply cmax. * induction (!cd1). apply dmax. - induction Ev. apply (squash_to_hProp W'w); intros [Ww|Ew]. + apply logeq_if_both_false. * assert (Q := cmax' (w,,Ww) W'v). unfold lt in Q. assert (e : (w,, W'w) = (subtype_inc j (w,, Ww))). { now apply subtypePath_prop. } induction e. exact Q. * assert (Q := dmax' (w,,Ww) W'd). unfold lt in Q. assert (e : (w,, W'w) = (subtype_inc j (w,, Ww))). { now apply subtypePath_prop. } induction e. assert (e : subtype_inc W'D (pr1 c,, W'v) = subtype_inc W'D (pr1 d,, W'd)). { now apply subtypePath_prop. } induction e. exact Q. + induction Ew. apply logeq_if_both_true ; now use TOeq_to_refl_1. } } assert (K := max_common_initial_is_max C D W' ci); fold W in K. assert (Wc : W (pr1 c)). { exact (K (pr1 c) W'c). } assert (L := pr1 (cE (pr1 c)) Wc). induction L as [Cc Q]. change (neg (c ≤ pr1 c,, Cc)) in Q. apply Q; clear Q. simple refine (transportf (λ c', c ≤ c') _ (TOrefl C c)). now apply subtypePath_prop. } change (wosub_comparable C D). unfold wosub_comparable. apply (squash_to_hProp E); clear E; intros E. apply hinhpr. Set Printing Coercions. induction E as [eWC|eWD]. - apply ii1. assert (e : W = C). { now apply hsubtype_univalence. } unfold W in *. clear W. induction (!e); clear e. use tpair. { exact WD. } split. { intros x y le. apply (pr1 (WCD x y)). now apply (h1'' le). } exact WDi. - apply ii2. assert (e : W = D). { now apply hsubtype_univalence. } unfold W in *. clear W. induction (!e); clear e. use tpair. { exact WC. } split. { intros x y le. apply (pr2 (WCD x y)). now apply (h1'' le). } exact WCi. Unset Printing Coercions. 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.