Martin Escardo, 17th December 2022.

Proof that in HoTT/UF the axiom of choice implies that every set can
be well-ordered, written in Agda, similar to the one in the HoTT book,
and to one of the two original proofs by Zermelo in set theory.

Converse added 22nd December 2022, but is already available, by Tom de
Jong since July 2021 in the module WellOrderingTaboo, which also shows
that, under excluded middle, the classical and inductive definitions
of ordinals agree.

\begin{code}

{-# OPTIONS --safe --without-K --lossy-unification #-}

open import MLTT.Spartan
open import NotionsOfDecidability.Decidable
open import Ordinals.Arithmetic
open import Ordinals.Equivalence
open import Ordinals.Notions
open import Ordinals.Type
open import Ordinals.Underlying
open import UF.Base
open import UF.Choice
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.ClassicalLogic
open import UF.FunExt
open import UF.Logic
open import UF.Powerset
open import UF.PropTrunc
open import UF.Sets
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt
open import UF.Univalence

\end{code}

We work in a Spartan Martin-LΓΆf type theory and assume that the
univalence axiom holds and that propositional truncations exist:

\begin{code}

module Ordinals.WellOrderingPrinciple
        (ua : Univalence)
        (pt : propositional-truncations-exist)
       where

open import Ordinals.BuraliForti ua
open import Ordinals.OrdinalOfOrdinals ua

\end{code}

We then derive function extensionality and propositional
extensionality from univalence:

\begin{code}

private
 fe : FunExt
 fe = Univalence-gives-FunExt ua

 fe' : Fun-Ext
 fe' {𝓀} {π“₯} = fe 𝓀 π“₯

 pe : Prop-Ext
 pe = Univalence-gives-Prop-Ext ua

 pe' : PropExt
 pe' 𝓀 = pe {𝓀}

open import Ordinals.WellOrderingTaboo fe' pe

open InductiveWellOrder pt
open PropositionalTruncation pt
open UF.Choice.ExcludedMiddle pt fe
open UF.Choice.choice-functions pt pe' fe
open UF.Choice.Univalent-Choice fe pt

\end{code}

We now state the main theorem of this file, and its converse, where
the axiom of choice is formulated as in the HoTT book.

\begin{code}

every-set-can-be-well-ordered = {𝓀 : Universe} {X : 𝓀 Μ‡ }
                              β†’ is-set X
                              β†’ βˆƒ _β‰Ί_ κž‰ (X β†’ X β†’ 𝓀 Μ‡ ), (is-well-order _β‰Ί_)

choice-gives-well-ordering : Axiom-of-Choice
                           β†’ every-set-can-be-well-ordered

well-ordering-gives-choice : every-set-can-be-well-ordered
                           β†’ Axiom-of-Choice

\end{code}

We first prove that, under excluded middle, if a set has a given
choice function, then it can be equipped with a well ordering. Later
we will derive excluded middle from choice in order to apply this to
prove the main theorem.

\begin{code}

open import Ordinals.WellOrderTransport fe
open import UF.ImageAndSurjection pt

open UF.Powerset.inhabited-subsets pt
open UF.Logic.AllCombinators pt fe'

choice-function-gives-well-ordering :

        Excluded-Middle
      β†’ {X : 𝓀 Μ‡ }
      β†’ is-set X
      β†’ (Ξ£ Ξ΅ κž‰ (π“Ÿ X β†’ X) , ((A : π“Ÿ X) β†’ is-inhabited A β†’ Ξ΅ A ∈ A))
      β†’ Ξ£ _<_ κž‰ (X β†’ X β†’ 𝓀 Μ‡ ), (is-well-order _<_)

choice-function-gives-well-ordering {𝓀} em {X} X-is-set (Ξ΅ , Ξ΅-behaviour) = W
 where

\end{code}

We first define a function f : Ordinal 𝓀 β†’ X by transfinite recursion
as follows:

\begin{code}

   Ο• : (Ξ± : Ordinal 𝓀) β†’ (⟨ Ξ± ⟩ β†’ X) β†’ X
   Ο• Ξ± s = Ξ΅ ⁅ x κž‰ X ∣ β±― a κž‰ ⟨ Ξ± ⟩ , s a β‰’ x ⁆

   f : Ordinal 𝓀 β†’ X
   f = transfinite-recursion-on-OO X Ο•

\end{code}

For an ordinal α and a point a in the underlying set ⟨ α ⟩ of α, we
denote by Ξ± ↓ a the down set of a in Ξ±. This is an ordinal on its own,
and, by univalence, every ordinal Ξ² β‰Ί Ξ± is of the form Ξ± ↓ a. Using
this construction, we define a subset A Ξ± of X for each ordinal Ξ±, and
with this we can specify the recursive behaviour of f as follows:

\begin{code}

   A : Ordinal 𝓀 β†’ π“Ÿ X
   A Ξ± = ⁅ x κž‰ X ∣ β±― a κž‰ ⟨ Ξ± ⟩ , f (Ξ± ↓ a) β‰’ x ⁆

   f-behaviour : (Ξ± : Ordinal 𝓀) β†’ f Ξ± = Ξ΅ (A Ξ±)
   f-behaviour = transfinite-recursion-on-OO-behaviour X Ο•

\end{code}

The following properties of f should be self-explanatory:

\begin{code}

   f-lemma : (Ξ± : Ordinal 𝓀) β†’ is-inhabited (A Ξ±) β†’ (Ξ² : Ordinal 𝓀) β†’ Ξ² ⊲ Ξ± β†’ f Ξ± β‰  f Ξ²
   f-lemma Ξ± i Ξ² (a , refl) p = III
    where
     I = Ρ (A α)   =⟨ (f-behaviour α)⁻¹ ⟩
         f α       =⟨ p ⟩
         f (Ξ± ↓ a) ∎


     II : f (Ξ± ↓ a) ∈ A Ξ±
     II = transport (_∈ A α) I (Ρ-behaviour (A α) i)

     III : 𝟘
     III = II a refl

   f-is-conditionally-1-1 : (Ξ± Ξ² : Ordinal 𝓀)
                          β†’ is-inhabited (A Ξ±)
                          β†’ is-inhabited (A Ξ²)
                          β†’ Ξ± β‰  Ξ²
                          β†’ f Ξ± β‰  f Ξ²
   f-is-conditionally-1-1 α β i j ν = I (trichotomy _⊲_ fe' em ⊲-is-well-order α β)
    where
     I : (Ξ± ⊲ Ξ²) + (Ξ± = Ξ²) + (Ξ² ⊲ Ξ±) β†’ f Ξ± β‰  f Ξ²
     I (inl l)       = β‰ -sym (f-lemma Ξ² j Ξ± l)
     I (inr (inl p)) = 𝟘-elim (ν p)
     I (inr (inr m)) = f-lemma Ξ± i Ξ² m

   f-is-conditionally-lc : (Ξ± Ξ² : Ordinal 𝓀)
                         β†’ is-inhabited (A Ξ±)
                         β†’ is-inhabited (A Ξ²)
                         β†’ f Ξ± = f Ξ²
                         β†’ Ξ± = Ξ²
   f-is-conditionally-lc Ξ± Ξ² i j p =
     ¬¬-elim
       (em (Ξ± = Ξ²) (the-type-of-ordinals-is-a-set (ua 𝓀) fe'))
       (Ξ» (Ξ½ : Ξ± β‰  Ξ²) β†’ f-is-conditionally-1-1 Ξ± Ξ² i j Ξ½ p)

\end{code}

A crucial property of the family A Ξ± of subsets of X is that it is
eventually empty. We first prove that it is somewhere empty by
contradiction, using the fact that the type of ordinals is large (by
the Burali-Forti argument). We need to use propositional resizing for
this purpose, which follows from excluded middle, which we are
assuming.

\begin{code}

   A-is-somewhere-empty : βˆƒ Ξ± κž‰ Ordinal 𝓀 , is-empty-subset (A Ξ±)
   A-is-somewhere-empty = III
    where
     I : Β¬ ((Ξ± : Ordinal 𝓀) β†’ is-inhabited (A Ξ±))
     I Ο• = absurd
      where
       f-lc : left-cancellable f
       f-lc {Ξ±} {Ξ²} = f-is-conditionally-lc Ξ± Ξ² (Ο• Ξ±) (Ο• Ξ²)

       f-is-embedding : is-embedding f
       f-is-embedding = lc-maps-into-sets-are-embeddings f f-lc X-is-set

       X' : 𝓀 ⁺ Μ‡
       X' = image f

       f' : Ordinal 𝓀 β†’ X'
       f' = corestriction f

       f'-is-equiv : is-equiv f'
       f'-is-equiv = corestriction-of-embedding-is-equivalence f f-is-embedding

       B : X β†’ 𝓀 ⁺ Μ‡
       B x = x ∈image f

       B-is-prop : (x : X) β†’ is-prop (B x)
       B-is-prop x = being-in-the-image-is-prop x f

       ρ : Propositional-Resizing
       ρ = EM-gives-PR em

       C : X β†’ 𝓀 Μ‡
       C x = resize ρ (B x) (B-is-prop x)

       Ο„ : Nat C B
       Ο„ x = from-resize ρ (B x) (B-is-prop x)

       Ο„-is-equiv : (x : X) β†’ is-equiv (Ο„ x)
       Ο„-is-equiv x = from-resize-is-equiv ρ (B x) (B-is-prop x)

       X'' : 𝓀 Μ‡
       X'' = Ξ£ x κž‰ X , C x

       e = X''       β‰ƒβŸ¨ NatΞ£ Ο„ , NatΞ£-is-equiv C B Ο„ Ο„-is-equiv ⟩
           X'        β‰ƒβŸ¨ ≃-sym (f' , f'-is-equiv) ⟩
           Ordinal 𝓀 β– 

       the-type-of-ordinals-is-small : is-small (Ordinal 𝓀)
       the-type-of-ordinals-is-small = X'' , e

       absurd : 𝟘
       absurd = the-type-of-ordinals-is-large the-type-of-ordinals-is-small

     II : βˆƒ Ξ± κž‰ Ordinal 𝓀 , Β¬ is-inhabited (A Ξ±)
     II = not-Ξ -implies-βˆƒ-not pt em (Ξ» x β†’ being-inhabited-is-prop (A x)) I

     III : βˆƒ Ξ± κž‰ Ordinal 𝓀 , is-empty-subset (A Ξ±)
     III = Natβˆƒ (Ξ» Ξ± β†’ non-inhabited-subsets-are-empty (A Ξ±)) II

\end{code}

It follows from the above and excluded middle that there is a least
such Ξ±, which we will call Ξ±β‚€:

\begin{code}

   A-is-eventually-empty : Ξ£ Ξ±β‚€ κž‰ Ordinal 𝓀
                                , is-empty-subset (A Ξ±β‚€)
                                Γ— ((Ξ± : Ordinal 𝓀) β†’ is-empty-subset (A Ξ±) β†’ Ξ±β‚€ β‰Ό Ξ±)
   A-is-eventually-empty = nonempty-has-minimal _⊲_ fe' em pt ⊲-is-well-order _
                            (Ξ» Ξ± β†’ being-empty-subset-is-prop fe' (A Ξ±))
                            A-is-somewhere-empty

   Ξ±β‚€ : Ordinal 𝓀
   eβ‚€ : is-empty-subset (A Ξ±β‚€)
   mβ‚€ : (Ξ± : Ordinal 𝓀) β†’ is-empty-subset (A Ξ±) β†’ Ξ±β‚€ β‰Ό Ξ±

   Ξ±β‚€ = pr₁ A-is-eventually-empty
   eβ‚€ = pr₁ (prβ‚‚ A-is-eventually-empty)
   mβ‚€ = prβ‚‚ (prβ‚‚ A-is-eventually-empty)

   nβ‚€ : (Ξ± : Ordinal 𝓀) β†’ Ξ± ⊲ Ξ±β‚€ β†’ is-inhabited (A Ξ±)
   nβ‚€ Ξ± l = non-empty-subsets-are-inhabited em
             (A Ξ±)
             (contrapositive (mβ‚€ Ξ±) (Ξ» (m : Ξ±β‚€ β‰Ό Ξ±) β†’ irrefl (OO 𝓀) Ξ± (m Ξ± l)))

\end{code}

We now restrict f to Ξ±β‚€ as follows, and show that the resulting map is
a surjection and an injection, and hence an equivalence, and we use
this to transport the well-ordering of Ξ±β‚€ to X to establish the
desired result:

\begin{code}

   fβ‚€ : ⟨ Ξ±β‚€ ⟩ β†’ X
   fβ‚€ a = f (Ξ±β‚€ ↓ a)

   fβ‚€-is-surjection : is-surjection fβ‚€
   fβ‚€-is-surjection x = not-Ξ -not-implies-βˆƒ pt em (eβ‚€ x)

   fβ‚€-lc : left-cancellable fβ‚€
   fβ‚€-lc {a} {b} p = II
    where
     Ia : is-inhabited (A (Ξ±β‚€ ↓ a))
     Ia = nβ‚€ (Ξ±β‚€ ↓ a) (a , refl)

     Ib : is-inhabited (A (Ξ±β‚€ ↓ b))
     Ib = nβ‚€ (Ξ±β‚€ ↓ b) (b , refl)

     I : (Ξ±β‚€ ↓ a) = (Ξ±β‚€ ↓ b)
     I = f-is-conditionally-lc (Ξ±β‚€ ↓ a) (Ξ±β‚€ ↓ b) Ia Ib p

     II : a = b
     II = ↓-lc Ξ±β‚€ a b I

   fβ‚€-is-embedding : is-embedding fβ‚€
   fβ‚€-is-embedding = lc-maps-into-sets-are-embeddings fβ‚€ fβ‚€-lc X-is-set

   fβ‚€-is-equiv : is-equiv fβ‚€
   fβ‚€-is-equiv = surjective-embeddings-are-equivs fβ‚€ fβ‚€-is-embedding fβ‚€-is-surjection

   structure-equiv : OrdinalStructure ⟨ Ξ±β‚€ ⟩ ≃ OrdinalStructure X
   structure-equiv = transport-ordinal-structure (ua 𝓀) ⟨ Ξ±β‚€ ⟩ X (fβ‚€ , fβ‚€-is-equiv)

\end{code}

And our desired results follows directly from this:

\begin{code}

   W : Ξ£ _<_ κž‰ (X β†’ X β†’ 𝓀 Μ‡ ), (is-well-order _<_)
   W = ⌜ structure-equiv ⌝ (structure Ξ±β‚€)

\end{code}

Using this we can prove the main theorem stated above, and restated
below, as follows. We first obtain a choice function conditionally to
the inhabitedness of X from the axiom of choice, and also the
principle of excluded middle. We then use excluded middle to check
whether X is inhabited. If it is, we apply the above lemma. Otherwise
it is empty and hence clearly well-ordered.

\begin{code}

choice-gives-well-ordering = restatement
 where
  restatement : Axiom-of-Choice
              β†’ {𝓀 : Universe} {X : 𝓀 Μ‡ }
              β†’ is-set X
              β†’ βˆƒ _<_ κž‰ (X β†’ X β†’ 𝓀 Μ‡ ), (is-well-order _<_)
  restatement ac {𝓀} {X} X-is-set = III
   where
    choice-function : βˆ₯ X βˆ₯ β†’ βˆƒ Ξ΅ κž‰ (π“Ÿ X β†’ X) , ((A : π“Ÿ X) β†’ is-inhabited A β†’ Ξ΅ A ∈ A)
    choice-function = Choice-gives-Choiceβ‚„ ac X X-is-set

    em : Excluded-Middle
    em = Choice-gives-Excluded-Middle pe' ac

    I : βˆ₯ X βˆ₯ β†’ βˆƒ _<_ κž‰ (X β†’ X β†’ 𝓀 Μ‡ ), (is-well-order _<_)
    I s = βˆ₯βˆ₯-functor
            (choice-function-gives-well-ordering em X-is-set)
            (choice-function s)

    II : Β¬ βˆ₯ X βˆ₯ β†’ βˆƒ _<_ κž‰ (X β†’ X β†’ 𝓀 Μ‡ ), (is-well-order _<_)
    II ν = ∣ structure (prop-ordinal fe X (empty-types-are-props (ν ∘ ∣_∣))) ∣

    III : βˆƒ _<_ κž‰ (X β†’ X β†’ 𝓀 Μ‡ ), (is-well-order _<_)
    III = cases I II (em βˆ₯ X βˆ₯ βˆ₯βˆ₯-is-prop)

\end{code}

We now prove the converse of the main theorem.

\begin{code}

well-ordering-gives-choice-function :

        Excluded-Middle
      β†’ {X : 𝓀 Μ‡ }
      β†’ is-set X
      β†’ Ξ£ _<_ κž‰ (X β†’ X β†’ 𝓀 Μ‡ ), (is-well-order _<_)
      β†’ (Ξ£ Ξ΅ κž‰ (π“ŸβΊ X β†’ X) , ((𝓐 : π“ŸβΊ X) β†’ Ξ΅ 𝓐 ∈⁺ 𝓐))

well-ordering-gives-choice-function {𝓀} em {X} X-is-set (_<_ , w) = Ξ΅ , Ξ΅-behaviour
 where
  ΞΌ : (𝓐 : π“ŸβΊ X) β†’ Ξ£ xβ‚€ κž‰ X , (xβ‚€ ∈⁺ 𝓐) Γ— _
  μ (A , i) = nonempty-has-minimal _<_ fe' em pt w (_∈ A) (∈-is-prop A) i

  Ξ΅ : π“ŸβΊ X β†’ X
  Ξ΅ 𝓐 = pr₁ (ΞΌ 𝓐)

  Ξ΅-behaviour : (𝓐 : π“ŸβΊ X) β†’ Ξ΅ 𝓐 ∈⁺ 𝓐
  Ξ΅-behaviour 𝓐 = pr₁ (prβ‚‚ (ΞΌ 𝓐))

well-ordering-gives-choice = restatement
 where
  restatement : every-set-can-be-well-ordered β†’ Axiom-of-Choice
  restatement w {𝓀} {π“₯} = II
   where
    em : Excluded-Middle
    em = inductive-well-order-on-every-set-gives-excluded-middle (Ξ» _ β†’ w)

    I : AC₃ {𝓀 βŠ” π“₯}
    I X X-is-set = βˆ₯βˆ₯-functor
                    (well-ordering-gives-choice-function em X-is-set)
                    (w X-is-set)

    II : AC {𝓀} {π“₯}
    II = AC₃-gives-AC I

\end{code}