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 (Ξ± β 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}