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 --safe --without-K #-}

open import MLTT.Spartan

open import UF.Base hiding (_β_)
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.ClassicalLogic
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.Sets-Properties
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

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

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

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

\end{code}

MartΓ­n EscadΓ³ observed that extensionality for minimal elements is logically
equivalent to the arguably simpler condition that there is at most one minimal
element.

This observation was implicitly used in some of the proofs below. Since MartΓ­n's
observation and adding a proof of the equivalence, the uses have been made
explicit.

\begin{code}

having-at-most-one-minimal-element : π€ β π£ Μ
having-at-most-one-minimal-element = is-prop (Ξ£ x κ X , ((y : X) β Β¬ (y βΊ x)))

extensionality-for-minimal-elts-if-at-most-one-minimal-elt :
having-at-most-one-minimal-element β extensionality-for-minimal-elements
extensionality-for-minimal-elts-if-at-most-one-minimal-elt
at-most-one-min x y x-min y-min x-y-ext = goal
where
claim : (x , x-min οΌ y , y-min)
claim = at-most-one-min (x , x-min) (y , y-min)
goal : x οΌ y
goal =  ap prβ claim

at-most-one-minimal-elt-if-extensionality-for-minimal-elts :
extensionality-for-minimal-elements β having-at-most-one-minimal-element
at-most-one-minimal-elt-if-extensionality-for-minimal-elts
ext (x , x-min) (y , y-min) = goal
where
claim : (a : X) β (a βΊ x) β (a βΊ y)
claim a = (I , II)
where
I : a βΊ x β a βΊ y
I p = π-elim (x-min a p)
II : a βΊ y β a βΊ x
II q = π-elim (y-min a q)
goal : (x , x-min) οΌ (y , y-min)
goal = to-subtype-οΌ I II
where
I : (b : X) β is-prop ((a : X) β Β¬ (a βΊ b))
I b = Ξ -is-prop fe (Ξ» a β negations-are-props fe)
II : x οΌ y
II = ext x y x-min y-min claim

\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 = goal
where
x-min : (a : S) β Β¬ (a βΊ x)
x-min a = all-elements-are-minimal a x
y-min : (a : S) β Β¬ (a βΊ y)
y-min a = all-elements-are-minimal a y
claim : (x , x-min) οΌ (y , y-min)
claim = at-most-one-minimal-elt-if-extensionality-for-minimal-elts
_βΊ_ βΊ-minimally-extensional (x , x-min) (y , y-min)
goal : x οΌ y
goal = ap prβ claim

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 , Β¬Β¬-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 Ordinals.Notions

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 PropositionalTruncation pt

open import MLTT.Two-Properties

open import Quotient.Type
open import Quotient.Large pt fe pe
open import UF.ImageAndSurjection pt

open general-set-quotients-exist large-set-quotients

_β_ : π β π β π€ Μ
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 β£

β : EqRel π
β = (_β_ , β-is-prop-valued , β-is-reflexive , β-is-symmetric , β-is-transitive)

S : π€ βΊ Μ
S = π / β

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

S-is-set : is-set S
S-is-set = /-is-set β

quotient-lemma : (x : S) β (x οΌ Ξ·/ β β) β¨ (x οΌ Ξ·/ β β)
quotient-lemma x = β₯β₯-functor Ξ³ (Ξ·/-is-surjection β pt 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 = Ξ·/-identifies-related-points β β£ 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 = Ξ·/-identifies-related-points β β£ inr p β£

β-identifies-β-and-β : Ξ·/ β β οΌ Ξ·/ β β
β-identifies-β-and-β = goal
where
claim : (Ξ·/ β β , Ξ·β-minimal) οΌ (Ξ·/ β β , Ξ·β-minimal)
claim = at-most-one-minimal-elt-if-extensionality-for-minimal-elts
_βΊ_ βΊ-minimally-extensional (Ξ·/ β β , Ξ·β-minimal) (Ξ·/ β β , Ξ·β-minimal)
goal : Ξ·/ β β οΌ Ξ·/ β β
goal = ap prβ claim

P-must-hold : P
P-must-hold =
β₯β₯-rec P-is-prop Ξ³ (large-effective-set-quotients β β-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 Ordinals.Notions _βΊ_

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-order
β (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 MLTT.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 = acc Ο
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 MLTT.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) Β¬Β¬-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 Ordinals.Notions
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
Ο : is-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 Univalent-Choice (Ξ» _ _ β 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β-gives-AC (ACβ-gives-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}