Tom de Jong, 22 & 23 July 2021 (following Andrew Swan)

After a discussion with Dominik Kirst on propositional resizing at FSCD 2021,
MartΓ­n EscardΓ³ asked the following question on HoTT Zulip [1] and nLab:

By an inductive well-ordering I mean a well ordering in the sense of the HoTT
book (accessible, extensional, transitive relation). If we assume that every
set can be inductively well ordered, can we conclude that excluded middle
holds?

Andrew Swan quickly answered this question positively, presenting two proofs
(based on the same idea). We formalize both proofs here.

In turns out that transitivity and accessibility are not needed, i.e. Swan
proves the much stronger result:

If every set has some irreflexive, extensional order, then excluded middle
follows.

In fact, we don't need full extensionality (as remarked by Dominik Kirst): it
suffices that we have extensionality for minimal elements.

It follows that the inductive well-ordering principle implies, and hence is
equivalent, to the axiom of choice. This is because we can reuse the classical
proof: first you get that inductive well-ordering implies classical well-ordering
(every non-empty subset has a minimal element), using excluded middle via the
argument above. Then we use the classical proof that (any kind of) well-ordering
implies choice.

[1] tinyurl.com/HoTT-Zulip-well-ordering

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

open import SpartanMLTT

open import UF-Base hiding (_β_)
open import UF-Equiv
open import UF-EquivalenceExamples
open import UF-ExcludedMiddle
open import UF-FunExt
open import UF-PropTrunc
open import UF-Subsingletons
open import UF-Subsingletons-FunExt

module WellOrderingTaboo
(fe  : Fun-Ext)
(pe  : Prop-Ext)
where

extensionality-for-minimal-elements : {X : π€ Μ } (_βΊ_ : X β X β π£ Μ )
β π€ β π£ Μ
extensionality-for-minimal-elements {π€} {π£} {X} _βΊ_ =
(x y : X) β ((a : X) β Β¬ (a βΊ x))
β ((a : X) β Β¬ (a βΊ y))
β ((a : X) β a βΊ x β a βΊ y) β x β‘ y

\end{code}

We first present Andrew Swan's second proof, which is a simplification of his
first proof that does not need exact quotients (we use propositional truncations
to construct quotients).

Because the main results *do* use propositional truncations to have the
existential quantifier β available, we only present those later, in order to
emphasize that Swan's construction does not need propositional truncations.

We construct a family of sets Sβ indexed by propositions P whose double negation
holds such that if Sβ can be equipped with an irreflexive and
minimally-extensional order, then the corresponding proposition P must hold.

\begin{code}

module swan
(P : π€ Μ )
(P-is-prop : is-prop P)
(P-is-not-false : Β¬Β¬ P)
where

S : π€ βΊ Μ
S = Ξ£ Q κ π€ Μ , is-prop Q Γ Β¬Β¬ (Q β‘ P)

S-is-set : is-set S
S-is-set = equiv-to-set (β-sym Ξ£-assoc) S'-is-set
where
S' : π€ βΊ Μ
S' = Ξ£ Q κ Ξ© π€ , Β¬Β¬ (Q holds β‘ P)
S'-is-set : is-set S'
S'-is-set = subtypes-of-sets-are-sets prβ (prβ-lc (negations-are-props fe))

all-elements-are-Β¬Β¬-equal : (x y : S) β Β¬Β¬ (x β‘ y)
all-elements-are-Β¬Β¬-equal (Q , i , t) (Q' , i' , t') = Β¬Β¬-kleisli Ξ³ t
where
Ξ³ : Q β‘ P β Β¬Β¬ ((Q , i , t) β‘ (Q' , i' , t'))
Ξ³ refl = Β¬Β¬-functor h t'
where
h : Q' β‘ P β (P , i , t) β‘ (Q' , i' , t')
h refl = to-subtype-β‘
(Ξ» _ β Γ-is-prop
(being-prop-is-prop fe)
(negations-are-props fe))
refl

module _
(_βΊ_ : S β S β π£ Μ )
(βΊ-irreflexive : (x : S) β Β¬ (x βΊ x))
(βΊ-minimally-extensional : extensionality-for-minimal-elements _βΊ_)
where

all-elements-are-minimal : (x y : S) β Β¬ (x βΊ y)
all-elements-are-minimal x y = contrapositive Ξ³ (all-elements-are-Β¬Β¬-equal x y)
where
Ξ³ : x βΊ y β Β¬ (x β‘ y)
Ξ³ l refl = βΊ-irreflexive x l

all-elements-are-equal : (x y : S) β x β‘ y
all-elements-are-equal x y = βΊ-minimally-extensional x y
(Ξ» s β all-elements-are-minimal s x)
(Ξ» s β all-elements-are-minimal s y)
Ξ³
where
Ξ³ : (s : S) β (s βΊ x) β (s βΊ y)
Ξ³ s = (f , g)
where
f : s βΊ x β s βΊ y
f l = π-elim (all-elements-are-minimal s x l)
g : s βΊ y β s βΊ x
g l = π-elim (all-elements-are-minimal s y l)

P-must-hold : P
P-must-hold = Idtofun Ξ³ *
where
Ξ³ : π β‘ P
Ξ³ = ap prβ (all-elements-are-equal π-in-S P-in-S)
where
P-in-S : S
P-in-S = (P , P-is-prop , double-negation-intro refl)
π-in-S : S
π-in-S = (π , π-is-prop , h)
where
h : Β¬Β¬ (π β‘ P)
h = Β¬Β¬-functor
(Ξ» p β pe π-is-prop P-is-prop (Ξ» _ β p) (Ξ» _ β *))
P-is-not-false

\end{code}

This construction allows us to prove the results announced above.

We first need some definitions.

\begin{code}

module InductiveWellOrder
(pt : propositional-truncations-exist)
where

open PropositionalTruncation pt

open import OrdinalNotions

irreflexive-minimally-extensional-order-on-every-set : (π€ π£ : Universe)
β (π€ β π£) βΊ Μ
irreflexive-minimally-extensional-order-on-every-set π€ π£ =
(X : π€ Μ ) β is-set X β β _βΊ_ κ (X β X β π£ Μ ) , ((x : X) β Β¬ (x βΊ x))
Γ (extensionality-for-minimal-elements _βΊ_)

irreflexive-extensional-order-on-every-set : (π€ π£ : Universe) β (π€ β π£) βΊ Μ
irreflexive-extensional-order-on-every-set π€ π£ =
(X : π€ Μ ) β is-set X β β _βΊ_ κ (X β X β π£ Μ ) , ((x : X) β Β¬ (x βΊ x))
Γ (is-extensional _βΊ_)

inductive-well-order-on-every-set : (π€ π£ : Universe) β (π€ β π£) βΊ Μ
inductive-well-order-on-every-set π€ π£ =
(X : π€ Μ ) β is-set X β β _βΊ_ κ (X β X β π£ Μ) , (is-well-order _βΊ_)

\end{code}

The following are the main theorems, which follow directly from Swan's results
above.

\begin{code}

irreflexive-minimally-extensional-order-on-every-set-gives-excluded-middle :
{π€ π£ : Universe} β irreflexive-minimally-extensional-order-on-every-set (π€ βΊ) π£
β excluded-middle π€
irreflexive-minimally-extensional-order-on-every-set-gives-excluded-middle
{π€} {π£} IMEO = DNE-gives-EM fe Ξ³
where
Ξ³ : DNE π€
Ξ³ P P-is-prop P-is-not-false = β₯β₯-rec P-is-prop h t
where
open swan P P-is-prop P-is-not-false
t : β _βΊ_ κ (S β S β π£ Μ) , ((x : S) β Β¬ (x βΊ x))
Γ (extensionality-for-minimal-elements _βΊ_)
t = IMEO S S-is-set
h : (Ξ£ _βΊ_ κ (S β S β π£ Μ) , ((x : S) β Β¬ (x βΊ x))
Γ (extensionality-for-minimal-elements _βΊ_))
β P
h (_βΊ_ , βΊ-irr , βΊ-min-ext) = P-must-hold _βΊ_ βΊ-irr βΊ-min-ext

irreflexive-extensional-order-on-every-set-gives-excluded-middle :
{π€ π£ : Universe} β irreflexive-extensional-order-on-every-set (π€ βΊ) π£
β excluded-middle π€
irreflexive-extensional-order-on-every-set-gives-excluded-middle {π€} {π£} IEO =
irreflexive-minimally-extensional-order-on-every-set-gives-excluded-middle Ξ³
where
Ξ³ : irreflexive-minimally-extensional-order-on-every-set (π€ βΊ) π£
Ξ³ X X-is-set = β₯β₯-functor f (IEO X X-is-set)
where
f : (Ξ£ _βΊ_ κ (X β X β π£ Μ) , ((x : X) β Β¬ (x βΊ x)) Γ (is-extensional _βΊ_))
β (Ξ£ _βΊ_ κ (X β X β π£ Μ) , ((x : X) β Β¬ (x βΊ x))
Γ (extensionality-for-minimal-elements _βΊ_))
f (_βΊ_ , βΊ-irr , βΊ-ext) = _βΊ_ , βΊ-irr , βΊ-min-ext
where
βΊ-min-ext : extensionality-for-minimal-elements _βΊ_
βΊ-min-ext x y _ _ e = extensional-gives-extensional' _βΊ_ βΊ-ext x y e

inductive-well-order-on-every-set-gives-excluded-middle :
{π€ π£ : Universe} β inductive-well-order-on-every-set (π€ βΊ) π£
β excluded-middle π€
inductive-well-order-on-every-set-gives-excluded-middle {π€} {π£} IWO =
irreflexive-extensional-order-on-every-set-gives-excluded-middle Ξ³
where
Ξ³ : irreflexive-extensional-order-on-every-set (π€ βΊ) π£
Ξ³ X X-is-set = β₯β₯-functor f (IWO X X-is-set)
where
f : (Ξ£ _βΊ_ κ (X β X β π£ Μ) , (is-well-order _βΊ_))
β (Ξ£ _βΊ_ κ (X β X β π£ Μ) , ((x : X) β Β¬ (x βΊ x)) Γ (is-extensional _βΊ_))
f (_βΊ_ , iwo) = (_βΊ_ , βΊ-irr , extensionality _βΊ_ iwo)
where
βΊ-irr : (x : X) β Β¬ (x βΊ x)
βΊ-irr x = irreflexive _βΊ_ x (well-foundedness _βΊ_ iwo x)

\end{code}

For comparison, we include Andrew Swan's first construction of the family of
sets, which could also be used to derive the above results. This construction
uses quotients, which we constuct using propositional truncations.

\begin{code}

module swan'
(pt  : propositional-truncations-exist)
(P : π€ Μ )
(P-is-prop : is-prop P)
(P-is-not-false : Β¬Β¬ P)
where

open import Two-Properties

open import UF-Quotient pt fe pe

open import UF-ImageAndSurjection
open ImageAndSurjection pt

open PropositionalTruncation pt

_β_ : π β π β π€ Μ
x β y = (x β‘ y) β¨ P

β-is-prop-valued : is-prop-valued _β_
β-is-prop-valued x y = β¨-is-prop

β-is-reflexive : reflexive _β_
β-is-reflexive x = β£ inl refl β£

β-is-symmetric : symmetric _β_
β-is-symmetric x y = β₯β₯-functor Ξ³
where
Ξ³ : (x β‘ y) + P β (y β‘ x) + P
Ξ³ (inl e) = inl (e β»ΒΉ)
Ξ³ (inr p) = inr p

β-is-transitive : transitive _β_
β-is-transitive x y z = β₯β₯-rec (Ξ -is-prop fe (Ξ» _ β β-is-prop-valued x z)) Ξ³
where
Ξ³ : (x β‘ y) + P β y β z β x β z
Ξ³ (inl eβ) = β₯β₯-functor Ο
where
Ο : (y β‘ z) + P β (x β‘ z) + P
Ο (inl eβ) = inl (eβ β eβ)
Ο (inr p)  = inr p
Ξ³ (inr p) _ = β£ inr p β£

open quotient π _β_
β-is-prop-valued β-is-reflexive β-is-symmetric β-is-transitive

S : π€ βΊ Μ
S = X/β

module _
(_βΊ_ : S β S β π£ Μ )
(βΊ-minimally-extensional : extensionality-for-minimal-elements _βΊ_)
(βΊ-irreflexive : (x : S) β Β¬ (x βΊ x))
where

S-is-set : is-set S
S-is-set = X/β-is-set

quotient-lemma : (x : S) β (x β‘ Ξ· β) β¨ (x β‘ Ξ· β)
quotient-lemma x = β₯β₯-functor Ξ³ (Ξ·-surjection x)
where
Ξ³ : (Ξ£ i κ π , Ξ· i β‘ x)
β (x β‘ Ξ· β) + (x β‘ Ξ· β)
Ξ³ (β , e) = inl (e β»ΒΉ)
Ξ³ (β , e) = inr (e β»ΒΉ)

Ξ·β-minimal : (x : S) β Β¬ (x βΊ Ξ· β)
Ξ·β-minimal x h = β₯β₯-rec π-is-prop Ξ³ (quotient-lemma x)
where
Ξ³ : (x β‘ Ξ· β) + (x β‘ Ξ· β) β π
Ξ³ (inl refl) = βΊ-irreflexive (Ξ· β) h
Ξ³ (inr refl) = P-is-not-false Ο
where
Ο : Β¬ P
Ο p = βΊ-irreflexive (Ξ· β) (transport (_βΊ (Ξ· β)) claim h)
where
claim : Ξ· β β‘ Ξ· β
claim = Ξ·-equiv-equal β£ inr p β£

Ξ·β-minimal : (x : S) β Β¬ (x βΊ Ξ· β)
Ξ·β-minimal x h = β₯β₯-rec π-is-prop Ξ³ (quotient-lemma x)
where
Ξ³ : (x β‘ Ξ· β) + (x β‘ Ξ· β) β π
Ξ³ (inr refl) = βΊ-irreflexive (Ξ· β) h
Ξ³ (inl refl) = P-is-not-false Ο
where
Ο : Β¬ P
Ο p = βΊ-irreflexive (Ξ· β) (transport (_βΊ (Ξ· β)) claim h)
where
claim : Ξ· β β‘ Ξ· β
claim = Ξ·-equiv-equal β£ inr p β£

β-identifies-β-and-β : Ξ· β β‘ Ξ· β
β-identifies-β-and-β = βΊ-minimally-extensional (Ξ· β) (Ξ· β)
Ξ·β-minimal Ξ·β-minimal Ξ³
where
Ξ³ : (s : S) β (s βΊ Ξ· β) β (s βΊ Ξ· β)
Ξ³ s = f , g
where
f : s βΊ Ξ· β β s βΊ Ξ· β
f h = π-elim (Ξ·β-minimal s h)
g : s βΊ Ξ· β β s βΊ Ξ· β
g h = π-elim (Ξ·β-minimal s h)

P-must-hold : P
P-must-hold =
β₯β₯-rec P-is-prop Ξ³ (Ξ·-equal-equiv β-identifies-β-and-β)
where
Ξ³ : (β β‘ β) + P β P
Ξ³ (inl e) = π-elim (zero-is-not-one e)
Ξ³ (inr p) = p

\end{code}

This concludes the formalization of Andrew Swan's proofs.

Next, we use the above argument to show that inductive well-ordering principle
implies the axiom of choice. This is because we can reuse the classical proof:
first you get the inductive well-ordering implies classical well-ordering (every
non-empty subset has a minimal element), using excluded middle via the argument
above. Then we use the classical proof that (any kind of) well-ordering implies
choice.

We start by defining classical well orders.

\begin{code}

module ClassicalWellOrder
(pt : propositional-truncations-exist)
where

open PropositionalTruncation pt

module _
{X : π€ Μ }
(_βΊ_ : X β X β π£ Μ )
where

open import OrdinalNotions _βΊ_

is-uniquely-trichotomous : π€ β π£ Μ
is-uniquely-trichotomous =
(x y : X) β is-singleton ((x βΊ y) + (x β‘ y) + (y βΊ x))

inhabited-has-minimal : (π€ β π£) βΊ Μ
inhabited-has-minimal = (A : X β (π€ β π£) Μ )
β ((x : X) β is-prop (A x))
β β x κ X , A x
β Ξ£ x κ X , A x Γ ((y : X) β A y β Β¬ (y βΊ x))

\end{code}

The definition inhabtited-has-minimal deserves two remarks:

(1) One may have expected β rather than Ξ£ in the conclusion, but in the presence
of trichotomy (which is an axiom of a classical well-order) the type
Ξ£ x κ X , A x Γ ((y : X) β A y β Β¬ (y βΊ x))
is a proposition, so there is no need to use β rather than Ξ£.

This result is minimal-is-prop below.

(2) We would like the above to express that every inhabited subset has a
minimal element, but in the absence of propositional resizing, this is tricky,
because it would require having an axiom *scheme* consisting of a definition
referring to families (A : X β π₯ Μ ) for each universe level π₯.

We don't wish to assume propsitional resizing here or have axiom schemes, so we
make the choice to use the universe π€ β π£. Recall that X : π€ and that _βΊ_ has
values in π£.

\begin{code}

minimal-is-prop : is-trichotomous
β (A : X β (π€ β π£) Μ )
β ((x : X) β is-prop (A x))
β is-prop (Ξ£ x κ X , A x Γ ((y : X) β A y β Β¬ (y βΊ x)))
minimal-is-prop trich A A-is-prop-valued (x , a , f) (x' , a' , f') =
to-subtype-β‘ i q
where
i : (x : X) β is-prop (A x Γ ((y : X) β A y β Β¬ (y βΊ x)))
i x = Γ-is-prop (A-is-prop-valued x) (Ξ β-is-prop fe (Ξ» x a l β π-is-prop))
q : x β‘ x'
q = ΞΊ (trich x x')
where
ΞΊ : (x βΊ x') + (x β‘ x') + (x' βΊ x) β x β‘ x'
ΞΊ (inl k)       = π-elim (f' x a k)
ΞΊ (inr (inl p)) = p
ΞΊ (inr (inr l)) = π-elim (f x' a' l)

is-classical-well-order : (π€ β π£) βΊ Μ
is-classical-well-order = is-transitive
Γ is-uniquely-trichotomous
Γ inhabited-has-minimal

\end{code}

Assuming excluded middle (for π€ β π£), we show

_βΊ_ is a classical well-order β _βΊ_ is an inductive well-order.

A remark on well-order-gives-minimal (see below) is in order.
It may seem that it repeats nonempty-has-minimal in OrdinalNotions.lagda, but
nonempty-has-minimal uses Β¬Β¬ and excluded middle in *every* universe to
construct propositional truncations, and β in particular, but we just assume
propositional truncations and when we assume excluded middle, we only do so
for specific universes.

\begin{code}

module _
(em : excluded-middle (π€ β π£))
where

open import Plus-Properties

well-order-gives-minimal : is-well-order
β inhabited-has-minimal
well-order-gives-minimal iwo A A-is-prop-valued A-is-inhabited = Ξ³
where
B : π€ β π£ Μ
B = Ξ£ x κ X , A x Γ ((y : X) β A y β Β¬ (y βΊ x))
B-is-prop : is-prop B
B-is-prop = minimal-is-prop (trichotomy fe em iwo) A A-is-prop-valued
Ξ΄ : Β¬Β¬ B
Ξ΄ f = β₯β₯-rec π-is-prop A-is-empty A-is-inhabited
where
Ο : (x : X) β ((y : X) β y βΊ x β Β¬ A y) β Β¬ A x
Ο x h a = β₯β₯-rec π-is-prop x-is-minimal claim
where
lemma : Β¬ ((y : X) β A y β Β¬ (y βΊ x))
lemma g = f (x , a , g)
x-is-minimal : Β¬ (Ξ£ (y , _) κ Ξ£ A , y βΊ x)
x-is-minimal ((y , a') , k) = h y k a'
claim : β Ο κ Ξ£ A , prβ Ο βΊ x
claim = not-Ξ -not-implies-β pt em lemma'
where
lemma' : Β¬ ((Ο : Ξ£ A) β Β¬ (prβ Ο βΊ x))
lemma' = contrapositive (Ξ» g' y p' β g' (y , p')) lemma
A-is-empty : is-empty (Ξ£ A)
A-is-empty (x , p) = A-is-false x p
where
A-is-false : (x : X) β Β¬ A x
A-is-false = transfinite-induction (well-foundedness iwo) (Ξ» x β Β¬ A x) Ο
Ξ³ : B
Ξ³ = EM-gives-DNE em B B-is-prop Ξ΄

inductive-well-order-is-classical : is-well-order
β is-classical-well-order
inductive-well-order-is-classical iwo =
(transitivity iwo , uniq-trich , well-order-gives-minimal iwo)
where
trich-prop : (x y : X) β is-prop ((x βΊ y) + (x β‘ y) + (y βΊ x))
trich-prop x y = +-is-prop (prop-valuedness iwo x y)
(+-is-prop (well-ordered-types-are-sets (Ξ» _ _ β fe) iwo)
(prop-valuedness iwo y x) Ο) Ο
where
Ο : x β‘ y β Β¬ (y βΊ x)
Ο refl = irreflexive x (well-foundedness iwo x)
Ο : x βΊ y β Β¬ ((x β‘ y) + (y βΊ x))
Ο k (inl refl) = irreflexive x (well-foundedness iwo x) k
Ο k (inr l)    = irreflexive x (well-foundedness iwo x)
(transitivity iwo x y x k l)
uniq-trich : is-uniquely-trichotomous
uniq-trich x y = pointed-props-are-singletons
(trichotomy fe em iwo x y)
(trich-prop x y)

minimal-gives-well-foundedness : inhabited-has-minimal
β is-well-founded
minimal-gives-well-foundedness min = Ξ³
where
Ξ΄ : (x : X) β Β¬Β¬ (is-accessible x)
Ξ΄ xβ xβ-not-acc = x-not-acc x-acc
where
B : X β π€ β π£ Μ
B x = Β¬ (is-accessible x)
m : Ξ£ x κ X , B x Γ ((y : X) β B y β Β¬ (y βΊ x))
m = min B (Ξ» _ β negations-are-props fe) β£ xβ , xβ-not-acc β£
x : X
x = prβ m
x-not-acc : B x
x-not-acc = prβ (prβ m)
x-minimal : (y : X) β B y β Β¬ (y βΊ x)
x-minimal = prβ (prβ m)
x-acc : is-accessible x
x-acc = next x Ο
where
Ξ΅ : (y : X) β y βΊ x β Β¬Β¬ (is-accessible y)
Ξ΅ y l y-not-acc = x-minimal y y-not-acc l
Ο : (y : X) β y βΊ x β is-accessible y
Ο y l = EM-gives-DNE em (is-accessible y) (accessibility-is-prop (Ξ» _ _ β fe) y) (Ξ΅ y l)
Ξ³ : is-well-founded
Ξ³ x = EM-gives-DNE em (is-accessible x) (accessibility-is-prop (Ξ» _ _ β fe) x) (Ξ΄ x)

classical-well-order-is-inductive : is-classical-well-order
β is-well-order
classical-well-order-is-inductive (trans , trich , min) =
pv , wf , ext , trans
where
pv : is-prop-valued
pv x y k l = inl-lc (singletons-are-props (trich x y) (inl k) (inl l))
wf : is-well-founded
wf = minimal-gives-well-foundedness min
ext : is-extensional
ext x y u v = ΞΊ (center (trich x y))
where
ΞΊ : (x βΊ y) + (x β‘ y) + (y βΊ x) β x β‘ y
ΞΊ (inl k)       = π-elim (irreflexive x (wf x) (v x k))
ΞΊ (inr (inl e)) = e
ΞΊ (inr (inr l)) = π-elim (irreflexive y (wf y) (u y l))

\end{code}

Having a classical well-order on every set allows us to derive excluded middle
with a fairly direct proof.

\begin{code}

open import UF-Miscelanea
open import Two-Properties
open import UF-UniverseEmbedding

classical-well-order-on-every-set : (π€ π£ : Universe) β (π€ β π£) βΊ Μ
classical-well-order-on-every-set π€ π£ =
(X : π€ Μ ) β is-set X β β _βΊ_ κ (X β X β π£ Μ) , (is-classical-well-order _βΊ_)

classical-well-order-on-every-set-gives-excluded-middle :
{π€ π£ : Universe} β classical-well-order-on-every-set π€ π£
β excluded-middle (π€ β π£)
classical-well-order-on-every-set-gives-excluded-middle {π€} {π£} CWO P P-is-prop =
β₯β₯-rec Ο Ξ³ (CWO π' π'-is-set)
where
π' : π€ Μ
π' = Lift π€ π
π'-is-set : is-set π'
π'-is-set = equiv-to-set (Lift-β π€ π) π-is-set
ΞΉ : π β π'
ΞΉ = lift π€
Ο : is-prop (P + Β¬ P)
Ο = +-is-prop P-is-prop (negations-are-props fe) double-negation-intro
Ξ³ : (Ξ£ _βΊ_ κ (π' β π' β π£ Μ ) , (is-classical-well-order _βΊ_)) β P + Β¬ P
Ξ³ (_βΊ_ , trans , trich , min) = ΞΊ (center (trich (ΞΉ β) (ΞΉ β)))
where
ΞΊ : (ΞΉ β βΊ ΞΉ β) + (ΞΉ β β‘ ΞΉ β) + (ΞΉ β βΊ ΞΉ β)
β P + Β¬ P
ΞΊ (inr (inl e)) = π-elim (zero-is-not-one (equivs-are-lc ΞΉ lift-is-equiv e))
ΞΊ (inl k)       = f (min A A-is-prop-valued A-is-inhabited)
where
A : π' β π€ β π£ Μ
A x = π-cases P π (lower x)
A-is-prop-valued : (x : π') β is-prop (A x)
A-is-prop-valued (β , _) = P-is-prop
A-is-prop-valued (β , _) = π-is-prop
A-is-inhabited : β A
A-is-inhabited = β£ ΞΉ β , * β£
f : (Ξ£ x κ π' , A x Γ ((y : π') β A y β Β¬ (y βΊ x)))
β P + Β¬ P
f ((β , _) , p , _) = inl p
f ((β , _) , _ , m) = inr (Ξ» p β m (ΞΉ β) p k)
ΞΊ (inr (inr l)) = g (min B B-is-prop-valued B-is-inhabited)
where
B : π' β π€ β π£ Μ
B x = π-cases π P (lower x)
B-is-prop-valued : (x : π') β is-prop (B x)
B-is-prop-valued (β , _) = π-is-prop
B-is-prop-valued (β , _) = P-is-prop
B-is-inhabited : β B
B-is-inhabited = β£ ΞΉ β , * β£
g : (Ξ£ x κ π' , B x Γ ((y : π') β B y β Β¬ (y βΊ x)))
β P + Β¬ P
g ((β , _) , _ , m) = inr (Ξ» p β m (ΞΉ β) p l)
g ((β , _) , p , _) = inl p

\end{code}

We assumed excluded middle to show that every classical well-order is an
inductive well-order. But if we assume that we have a classical well-order on
every set, then we can derive excluded middle. Hence, if every set admits some
classical well-order, then every set admits some inducive well-order.

\begin{code}

open import OrdinalNotions
open InductiveWellOrder pt

classical-well-ordering-implies-inductive-well-ordering :
{π€ π£ : Universe}
β classical-well-order-on-every-set π€ π£
β inductive-well-order-on-every-set π€ π£
classical-well-ordering-implies-inductive-well-ordering {π€} {π£} CWO X X-is-set =
β₯β₯-functor Ξ³ (CWO X X-is-set)
where
Ξ³ : (Ξ£ _βΊ_ κ (X β X β π£ Μ ) , (is-classical-well-order _βΊ_))
β Ξ£ _βΊ_ κ (X β X β π£ Μ ) , (is-well-order _βΊ_)
Ξ³ (_βΊ_ , cwo) = (_βΊ_ , classical-well-order-is-inductive _βΊ_ em cwo)
where
em : excluded-middle (π€ β π£)
em = classical-well-order-on-every-set-gives-excluded-middle CWO

\end{code}

The converse holds too (but note the change in universe levels) and depends on
the straightforward but tedious lemma lower-inductive-well-order-on-every-set
which expresses that if every set in some large universe can be inductively
well-ordered, then so can every set in a lower universe.

(NB. There are similar, but different technical lemmas in the file
OrdinalsWellOrderTransport.lagda.)

\begin{code}

inductive-well-ordering-implies-classical-well-ordering :
{π€ π£ : Universe}
β inductive-well-order-on-every-set ((π€ β π£) βΊ) π£
β classical-well-order-on-every-set π€ π£

lower-inductive-well-order-on-every-set : {π€ π£ π₯ : Universe}
β inductive-well-order-on-every-set (π€ β π₯) π£
β inductive-well-order-on-every-set π€ π£
lower-inductive-well-order-on-every-set {π€} {π£} {π₯} IWO X X-is-set = β₯β₯-functor Ξ³ iwo
where
X' : π€ β π₯ Μ
X' = Lift π₯ X
ΞΉ : X β X'
ΞΉ = lift π₯
X'-is-set : is-set X'
X'-is-set = equiv-to-set (Lift-β π₯ X) X-is-set
iwo : β _βΊ'_ κ (X' β X' β π£ Μ) , (is-well-order _βΊ'_)
iwo = IWO X' X'-is-set
Ξ³ : (Ξ£ _βΊ'_ κ (X' β X' β π£ Μ) , (is-well-order _βΊ'_))
β (Ξ£ _βΊ_ κ (X β X β π£ Μ) , (is-well-order _βΊ_))
Ξ³ (_βΊ'_ , pv' , wf' , ext' , trans') = (_βΊ_ , pv , wf , ext , trans)
where
_βΊ_ : X β X β π£ Μ
x βΊ y = ΞΉ x βΊ' ΞΉ y
pv : is-prop-valued _βΊ_
pv x y = pv' (ΞΉ x) (ΞΉ y)
wf : is-well-founded _βΊ_
wf = transfinite-induction-converse _βΊ_ Ο
where
Ο : Well-founded _βΊ_
Ο P h x = transfinite-induction _βΊ'_ wf' P' h' (ΞΉ x)
where
P' : X' β π€ β π£ Μ
P' = P β lower
h' : (x' : X') β ((y : X') β y βΊ' x' β P' y) β P' x'
h' x' Ο = h (lower x') (Ξ» y k β Ο (ΞΉ y) k)
ext : is-extensional _βΊ_
ext x y u v = equivs-are-lc ΞΉ lift-is-equiv
(ext' (ΞΉ x) (ΞΉ y)
(Ξ» x' k β u (lower x') k)
(Ξ» y' l β v (lower y') l))
trans : is-transitive _βΊ_
trans x y z k l = trans' (ΞΉ x) (ΞΉ y) (ΞΉ z) k l

inductive-well-ordering-implies-classical-well-ordering {π€} {π£} IWO X X-is-set =
β₯β₯-functor Ξ³ (lower-inductive-well-order-on-every-set IWO X X-is-set)
where
Ξ³ : (Ξ£ _βΊ_ κ (X β X β π£ Μ ) , (is-well-order _βΊ_))
β Ξ£ _βΊ_ κ (X β X β π£ Μ ) , (is-classical-well-order _βΊ_)
Ξ³ (_βΊ_ , iwo) = (_βΊ_ , inductive-well-order-is-classical _βΊ_ em iwo)
where
em : excluded-middle (π€ β π£)
em = inductive-well-order-on-every-set-gives-excluded-middle IWO

\end{code}

Finally, we use the above to show that having an inductive well-order on every
set implies the axiom of choice.

(In fact, they are equivalent by Zermelo's proof of the Well Ordering Theorem,
but we don't formalize this.)

\begin{code}

module _
(pt : propositional-truncations-exist)
where

open import UF-Retracts
open import UF-Choice

open UnivalentChoice (Ξ» _ _ β fe) pt

open PropositionalTruncation pt

open ClassicalWellOrder pt
open InductiveWellOrder pt

classical-well-ordering-implies-ac : classical-well-order-on-every-set (π€ β π£) π£
β AC (π€ β π£)
classical-well-ordering-implies-ac {π€} {π£} CWO =
AC'AC (π€ β π£) (AC''AC' (π€ β π£) Ξ³)
where
Ξ³ : (X : π€ β π£ Μ ) (Y : X β π€ β π£ Μ )
β is-set X
β ((x : X) β is-set (Y x))
β β₯ ((x : X) β β₯ Y x β₯ β Y x) β₯
Ξ³ X Y X-is-set Y-is-set-valued =
β₯β₯-functor f (CWO (Ξ£ Y) (Ξ£-is-set X-is-set Y-is-set-valued))
where
f : (Ξ£ _βΊ_ κ (Ξ£ Y β Ξ£ Y β π£ Μ ) , (is-classical-well-order _βΊ_))
β ((x : X) β β₯ Y x β₯ β Y x)
f (_βΊ_ , _ , _ , min) x y = transport Y x'-is-x y'
where
S : Ξ£ Y β π€ β π£ Μ
S (x' , _) = x' β‘ x
m : Ξ£ Ο κ (Ξ£ Y) , S Ο Γ ((Ο : Ξ£ Y) β S Ο β Β¬ (Ο βΊ Ο))
m = min S (Ξ» _ β X-is-set) (β₯β₯-functor (Ξ» y' β (x , y') , refl) y)
x' : X
x' = prβ (prβ m)
x'-is-x : x' β‘ x
x'-is-x = prβ (prβ m)
y' : Y x'
y' = prβ (prβ m)

classical-well-ordering-implies-ac-corollary :
classical-well-order-on-every-set π€ π€ β AC π€
classical-well-ordering-implies-ac-corollary {π€} =
classical-well-ordering-implies-ac {π€} {π€}

inductive-well-ordering-implies-ac :
inductive-well-order-on-every-set ((π€ βΊ) β (π£ βΊ)) π£
β AC (π€ β π£)
inductive-well-ordering-implies-ac {π€} {π£} =
classical-well-ordering-implies-ac {π€} {π£}
β inductive-well-ordering-implies-classical-well-ordering

inductive-well-ordering-implies-ac-corollary :
inductive-well-order-on-every-set (π€ βΊ) π€
β AC π€
inductive-well-ordering-implies-ac-corollary {π€} =
inductive-well-ordering-implies-ac {π€} {π€}

\end{code}