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}

Added 13 March 2022.

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))
                (Ξ©-is-set fe pe)

 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 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.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}