Theorem ZermeloWellOrdering {X:hSet} : AxiomOfChoice ⇒ ∃ R : hrel X, isWellOrder R. Proof. intros ac. assert (lem := AC_to_LEM ac). apply (squash_to_hProp (AC_to_choice_fun X ac)); intro g. set (S := guidedFamily g). set (Schain := guided_WOSubset_total g lem). set (W := ⋃ Schain). assert (Wguided : is_guided_WOSubset g W). { intros [w Ww]. apply (squash_to_hProp Ww); intros [C Cw]. change (hProptoType (C w)) in Cw. simpl. assert (Q := pr2 C (w,,Cw)); simpl in Q. simple refine (Q @ _); clear Q. assert (CW := chain_union_le S Schain C : C ≼ W). use upto'_eqn. - exact CW. - reflexivity. } assert (all : ∀ x, W x). { apply (proof_by_contradiction lem); intro n. assert (Q := negforall_to_existsneg _ lem n); clear n. change hfalse. set (znW := g (pr1 W,,Q) : ∑ z : X, ¬ pr1 W z). set (z := pr1 znW). set (nWz := pr2 znW : ¬ pr1 W z). set (W' := WOSubset_plus_point W z nWz lem). assert (W'z := subtype_plus_has_point W z : W' z). set (j := TOSubset_plus_point_incl W z nWz : W ⊆ W'). set (jmap := subtype_inc j). assert (W'guided : is_guided_WOSubset g W'). { unfold is_guided_WOSubset. intros [x W'x]. change (x = pr1 (g (@upto' X W' (x,, W'x))))%logic. apply (squash_to_hProp W'x); intros [Wx|ezx]. - assert (x_guided := Wguided (x,,Wx)). change (x = pr1 (g (@upto' X W (x,, Wx))))%type in x_guided. simple refine (x_guided @ _); clear x_guided. use upto'_eqn. + assert (WW' := TOSubset_plus_point_le W z nWz). induction WW' as [WW' comp]. exists WW'. split. * exact comp. * intros w w' Ww W'w' le. simple refine (TOSubset_plus_point_initial W z nWz w w' Ww W'w' _). now apply (h1'' le). + reflexivity. - induction ezx. change (pr1 (g (pr1 W,, Q)) = pr1 (g (@upto' X W' (z,, W'x)))). assert (e : (pr1 W,, Q) = @upto' X W' (z,, W'x)). { apply subtypePath_prop. apply (invmap (hsubtype_univalence _ _)). intros y. change (W y ⇔ @upto X W' (z,, W'x) y). split. - intros Wy. exists (j y Wy). unfold lt. intros le. induction (ishinh_irrel (ii2 (idpath z)) W'x). change empty in le. exact le. - intros [W'y yz]. apply (squash_to_hProp W'y); intros [Wy|ezy]. + exact Wy. + induction ezy. apply fromempty. unfold lt,hneg in yz. apply yz. induction (proofirrelevance_hProp _ W'y W'x). exact (TOrefl W' (z,, W'y)). } now induction e. } assert (W'W := chain_union_le S Schain (W',,W'guided) : W' ≼ W). assert (K := pr2 (subtype_inc (pr1 W'W) (z,,W'z)) : W z). exact (nWz K). } clear Wguided. apply hinhpr. induction W as [W R']. change (∏ x : X, W x)%type in all. change (WellOrdering X). assert (e : X = carrier_subset W). { apply (invmap (hSet_univalence _ _)). apply invweq. apply weqpr1. intros x. simpl in all. apply iscontraprop1. - apply propproperty. - apply all. } induction e. exact R'. 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.