Kelton OBrien, 31 May 2024

A proof that the Axiom of Choice implies Zorn's Lemma, as well as
relevant definitions.

\begin{code}

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

open import MLTT.Spartan
open import Ordinals.Equivalence
open import Ordinals.Type
open import Ordinals.Underlying
open import UF.Base
open import UF.Choice
open import UF.ClassicalLogic
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Logic
open import UF.Powerset-MultiUniverse
open import UF.PropTrunc
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import UF.UA-FunExt
open import UF.Univalence
open import UF.UniverseEmbedding

module OrderedTypes.ZornsLemma
 {𝓀 𝓣 : Universe}
 (pt : propositional-truncations-exist)
 (ua : Univalence)
 {X : 𝓀 Μ‡}
 (_β‰ͺ_ : X β†’ X β†’ 𝓣 Μ‡)
  where

open PropositionalTruncation pt
open import Ordinals.BuraliForti ua
open import Ordinals.OrdinalOfOrdinals ua
open import UF.ImageAndSurjection pt

fe : FunExt
fe = Univalence-gives-FunExt ua
pe : Prop-Ext
pe = Univalence-gives-Prop-Ext ua
pe' : PropExt
pe' 𝓀 = pe {𝓀}
fe' : Fun-Ext
fe' {𝓀} {π“₯} = fe 𝓀 π“₯

open UF.Choice.ExcludedMiddle pt fe
open UF.Choice.Univalent-Choice fe pt
open UF.Choice.choice-functions pt pe' fe
open UF.Logic.Existential pt
open UF.Logic.Universal fe'
open import OrderedTypes.Poset fe'
open import Ordinals.WellOrderingTaboo fe' pe
open inhabited-subsets pt

open PosetAxioms
open ClassicalWellOrder pt

_β‹˜_ : X β†’ X β†’ (𝓀 βŠ” 𝓣) Μ‡
a β‹˜ b =  a β‰ͺ b Γ— (a β‰  b)

is-chain : {π“₯ : Universe} β†’ (Y : π“Ÿ {π“₯} X ) β†’  (𝓀 βŠ” 𝓣 βŠ” π“₯) Μ‡
is-chain Y = (x y : X) β†’ x ∈ Y β†’ y ∈ Y β†’ (x β‰ͺ y ∨ y β‰ͺ x)

has-maximal-element-strong :  (𝓀 βŠ” 𝓣) Μ‡
has-maximal-element-strong = Ξ£ x κž‰ X , ((y : X) β†’ x β‰ͺ y β†’ x ＝ y)

has-maximal-element : (𝓀 βŠ” 𝓣) Μ‡
has-maximal-element = βˆƒ x κž‰ X , ((y : X) β†’ x β‰ͺ y β†’ x ＝ y)

all-chains-have-upper-bound : {π“₯ : Universe} β†’ (𝓀 βŠ” 𝓣 βŠ” (π“₯ ⁺))  Μ‡
all-chains-have-upper-bound {π“₯} =
 (Y : π“Ÿ {π“₯} X) β†’ (is-chain Y) β†’ Ξ£ x κž‰ X , (βˆ€ y β†’ y ∈ Y β†’ y β‰ͺ x)

\end{code}

The following is a formalization ofthe standard transfinite-induction-based
proof of Zorn's lemma. The closest informal analog to the proof can be found
here: https://math.stackexchange.com/a/2889205.
The primary differences between this proof and that proof are just ones of
how sets are treated (notice the lack of a particular poset P),
additional detail in things that are glossed over in the formal proof,
(e.g the proof that the chain allfbs is a chain is not given).
The proof idea is the same.

We do a proof by contradiction (which is why we have that double negation),
where we assume that even though all chains have a least upper bound,
the set at hand does not have a maximal element.
These assumptions allow us to construct a function `f' from the ordinals to X,
which is a set, which preserves order, is therefore left-cancellable, and again
in turn an equivalence. `f' being order preserving relies on the fact
that there is no maximal element, as otherwise `f' would (as defined)
map many ordinals to the maximal element.  An equivalence between the
ordinals and a set is impossible, so there must (not-not) be a
maximum.

While this is the core of the proof logic, the final result to be used
elsewhere is found below, and takes in more reasonable inputs.

\begin{code}

choice-function-gives-zorns-lemma
 : Excluded-Middle
 β†’ poset-axioms (_β‰ͺ_)
 β†’ all-chains-have-upper-bound
 β†’ (Ξ£ Ξ΅ κž‰ (π“Ÿ {𝓣 βŠ” 𝓀} X β†’ X) , ((A : π“Ÿ X) β†’ is-inhabited A β†’ Ξ΅ A ∈ A))
 β†’ has-maximal-element

choice-function-gives-zorns-lemma
 lem
 (X-is-set , β‰ͺ-prop , β‰ͺ-refl , β‰ͺ-trans , β‰ͺ-antisym )
 chains
 (Ξ΅ , Ξ΅-behaviour) =
  (Β¬Β¬Ξ£β†’βˆƒ pt dn (Ξ» no-max β†’ absurd no-max))
   where
    dn : {π“₯ : Universe } β†’ DNE π“₯
    dn {π“₯} = EM-gives-DNE lem

    eq-is-¬¬-stable : {x : X} {y : X } β†’  ¬¬-stable (x ＝ y)
    eq-is-¬¬-stable {x} {y} ¬¬x=y = dn (x ＝ y) (X-is-set) ¬¬x=y

    β‰ͺ-is-¬¬-stable : {x : X} {y : X} β†’ ¬¬-stable (x β‰ͺ y)
    β‰ͺ-is-¬¬-stable {x} {y} ¬¬ll = dn (x β‰ͺ y) (β‰ͺ-prop x y) ¬¬ll

    β‹˜-prop : (a : X) β†’ (b : X) β†’ is-prop (a β‹˜ b)
    β‹˜-prop a b = Γ—-is-prop (β‰ͺ-prop a b) (negations-are-props fe')

    β‰ͺ-trans-β‹˜ : (x y z : X) β†’  x β‰ͺ y β†’ y β‹˜ z β†’ x β‹˜ z
    β‰ͺ-trans-β‹˜ x y z xβ‰ͺy (yβ‰ͺz , yβ‰ z) =
     β‰ͺ-trans x y z xβ‰ͺy yβ‰ͺz ,
      Ξ» x=z β†’ yβ‰ z ((β‰ͺ-antisym y z) yβ‰ͺz (transport (Ξ» q β†’ q β‰ͺ y) x=z xβ‰ͺy))

    g : (Ξ± : Ordinal 𝓀) β†’ ( ⟨ Ξ± ⟩ β†’ X) β†’ X
    g Ξ± s = Ξ΅  ⁅ x κž‰ X ∣ β±― a κž‰ ⟨ Ξ± ⟩ , (( s a β‹˜ x ) , β‹˜-prop (s a) x ) ⁆

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

    A : Ordinal 𝓀 β†’ π“Ÿ { (𝓀 βŠ” 𝓣) } X
    A Ξ± = ⁅ x κž‰ X ∣ β±― a κž‰ ⟨ Ξ± ⟩ , (f (Ξ± ↓ a) β‹˜ x , β‹˜-prop (f (Ξ± ↓ a)) x ) ⁆

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

    ⊲-is-classical-well-order : is-classical-well-order (_⊲_ {𝓀})
    ⊲-is-classical-well-order =
      inductive-well-order-is-classical _⊲_ lem ⊲-is-well-order

    ⊲-is-trichotomous : {a b : Ordinal 𝓀} β†’ (a ⊲ b) + (a ＝ b) + (b ⊲ a)
    ⊲-is-trichotomous {a} {b} = pr₁ (( pr₁ (prβ‚‚ ⊲-is-classical-well-order)) a b)

    f-preserves-order : Β¬ has-maximal-element-strong
                      β†’ (Ξ± Ξ² : Ordinal 𝓀)
                      β†’ Ξ² ⊲ Ξ±
                      β†’ f Ξ² β‹˜ f Ξ±
    f-preserves-order no-max = transfinite-induction-on-OO P (v no-max)
     where
      P : Ordinal 𝓀 β†’ (𝓀 ⁺ βŠ” 𝓣) Μ‡
      P Ξ± = βˆ€ Ξ² β†’ Ξ² ⊲ Ξ± β†’ f Ξ² β‹˜ f Ξ±
      v : Β¬ has-maximal-element-strong
        β†’ (Ξ± : Ordinal 𝓀)
        β†’ ((a : ⟨ Ξ± ⟩) β†’ P (Ξ± ↓ a))
        β†’ P Ξ±
      v no-max Ξ± s Ξ² (a , Ξ²=α↓a) =
       transport⁻¹ (Ξ» q β†’ f q β‹˜ f Ξ±) Ξ²=α↓a
        (transport⁻¹ (Ξ» q β†’ f (Ξ± ↓ a) β‹˜ q) (f-behaviour Ξ±) (step a))
       where
        allfb : π“Ÿ  X
        allfb = ⁅ x κž‰ X ∣ Ǝ Ξ²' , ((Ξ²' ⊲ Ξ± ) Γ— (x ＝ (f Ξ²'))) ⁆

        untrunc-works : (x y : X)
                      β†’ (Ξ£ Ξ²' κž‰ Ordinal 𝓀 , ((Ξ²' ⊲ Ξ±) Γ— (x ＝ f Ξ²')))
                      β†’ (Ξ£ Ξ²'' κž‰ Ordinal 𝓀 , ((Ξ²'' ⊲ Ξ±) Γ— (y ＝ f Ξ²'')))
                      β†’ x β‰ͺ y + y β‰ͺ x
        untrunc-works
         x
         y
         (Ξ²' , ((b' , Ξ²'=α↓b') , x=fΞ²'))
         (Ξ²'' , ((b'' , Ξ²''=α↓b'') , y=fΞ²''))
         = cases less (cases equal more) ⊲-is-trichotomous
         where
          less : Ξ²'' ⊲ Ξ²' β†’ (x β‰ͺ y + y β‰ͺ x)
          less b''<b' =
           inr (transport⁻¹ (Ξ» q β†’ y β‰ͺ q) x=fΞ²'
            (transport⁻¹ (Ξ» q β†’ q β‰ͺ f Ξ²') y=fΞ²''
              (pr₁ (transport⁻¹ (Ξ» q β†’ f Ξ²'' β‹˜ f q) Ξ²'=α↓b' ((s b') Ξ²''
               (transport (Ξ» q β†’ Ξ²'' ⊲ q) Ξ²'=α↓b' b''<b'))))))
          equal : Ξ²'' ＝ Ξ²' β†’ (x β‰ͺ y + y β‰ͺ x)
          equal b''=b' =
           inr (transport (Ξ» q β†’ y β‰ͺ q)
            (transport⁻¹ (Ξ» q β†’ y ＝ q) x=fΞ²'
             (transport⁻¹ (Ξ» q β†’ q ＝ f Ξ²') y=fΞ²'' (ap f b''=b'))) (β‰ͺ-refl y))

          more : Ξ²' ⊲ Ξ²'' β†’ (x β‰ͺ y + y β‰ͺ x)
          more b'<b'' =
            inl (transport⁻¹ (Ξ» q β†’ x β‰ͺ q) y=fΞ²''
             (transport⁻¹ (Ξ» q β†’ q β‰ͺ f Ξ²'') x=fΞ²'
              (pr₁ (transport⁻¹ (Ξ» q β†’ f Ξ²' β‹˜ f q) Ξ²''=α↓b''
               ((s b'') Ξ²' (transport (Ξ» q β†’ Ξ²' ⊲ q) Ξ²''=α↓b'' b'<b''))))))
        has-max-neg : (x : X) β†’ ¬¬ (Ξ£ y κž‰ X , Β¬ (x β‰ͺ y β†’ x ＝ y))
        has-max-neg x =
         not-Ξ -implies-not-not-Ξ£ (Ξ» z β†’ β†’-is-¬¬-stable eq-is-¬¬-stable)
          ((not-Ξ£-implies-Ξ -not no-max) x)

        allfb-is-chain :  is-chain allfb
        allfb-is-chain x y = βˆ₯βˆ₯-functorβ‚‚ (untrunc-works x y)

        allfb-has-ub : Ξ£ x κž‰ X , (βˆ€ y β†’ y ∈ allfb β†’ y β‰ͺ x)
        allfb-has-ub = chains allfb allfb-is-chain

        ub : X
        ub = pr₁ allfb-has-ub

        ub-is-ub : βˆ€ y β†’ y ∈ allfb β†’ y β‰ͺ ub
        ub-is-ub = prβ‚‚ allfb-has-ub

        ub-is-strict'
         : (Ξ£ q κž‰ X , (Β¬ ( ub β‰ͺ q β†’ ub ＝ q)))
         β†’ Ξ£ z κž‰ X , (βˆ€ y β†’ y ∈ allfb β†’ y β‹˜ z)
        ub-is-strict' (q , foo) =  q ,
         Ξ» y yin β†’ β‰ͺ-trans-β‹˜ y ub q (ub-is-ub y yin)
          ((β‰ͺ-is-¬¬-stable (pr₁ (negation-of-implication foo)))
           , (prβ‚‚ (negation-of-implication foo)))

        ub-is-strict : βˆƒ z κž‰ X , (βˆ€ y β†’ y ∈ allfb β†’ y β‹˜ z)
        ub-is-strict = (βˆ₯βˆ₯-functor ub-is-strict') (Β¬Β¬Ξ£β†’βˆƒ pt dn (has-max-neg ub))

        AΞ±-inhabited' :  Ξ£ x κž‰ X , (βˆ€ y β†’ y ∈ allfb β†’ y β‹˜ x)
                         β†’  Ξ£ x κž‰ X , ((i : ⟨ Ξ± ⟩) β†’ f (Ξ± ↓ i) β‹˜ x)
        AΞ±-inhabited' (x , ylt) =
         x ,  Ξ» i β†’  ylt (f (Ξ± ↓ i))  ∣  (Ξ± ↓ i) ,  ( ( i , refl )) , refl ∣

        AΞ±-inhabited :  βˆƒ x κž‰ X , (βˆ€ y β†’ y ∈ allfb β†’ y β‹˜ x) β†’ is-inhabited (A Ξ±)
        AΞ±-inhabited =  βˆ₯βˆ₯-functor AΞ±-inhabited'

        step : (a : ⟨ Ξ± ⟩) β†’  (f (Ξ± ↓ a) β‹˜ Ξ΅ (A Ξ±))
        step a = (Ξ΅-behaviour (A Ξ±) (AΞ±-inhabited (ub-is-strict ))) a

    f-is-injective : Β¬ has-maximal-element-strong
                   β†’ (a b : Ordinal 𝓀)
                   β†’ a β‰  b β†’ f a β‰  f b
    f-is-injective no-max a b a≠b =
     cases (less a b) (cases (equal a b aβ‰ b) (more a b)) ⊲-is-trichotomous
     where
      less : (a b : Ordinal 𝓀) β†’ a ⊲ b β†’ f a β‰  f b
      less a b a<b = prβ‚‚ (f-preserves-order no-max b a a<b)

      more : (a b : Ordinal 𝓀) β†’ b ⊲ a β†’ f a β‰  f b
      more a b b<a = β‰ -sym (prβ‚‚ (f-preserves-order no-max a b b<a))

      equal : (a b : Ordinal 𝓀) β†’ a β‰  b β†’ a ＝ b β†’ f a β‰  f b
      equal a b aβ‰ b a=b = unique-from-𝟘 (aβ‰ b a=b)

    f-is-left-cancellable
     : {a : Ordinal 𝓀}
     β†’ {b : Ordinal 𝓀}
     β†’ Β¬ has-maximal-element-strong
     β†’ f a ＝ f b
     β†’ a ＝ b
    f-is-left-cancellable {a} {b} no-max p =
     dn (a ＝ b) (the-type-of-ordinals-is-a-set (ua 𝓀) fe')
                 ((contrapositive (f-is-injective no-max a b)) (¬¬-intro p))

    f-is-embedding : Β¬ has-maximal-element-strong β†’ is-embedding f
    f-is-embedding no-max = lc-maps-into-sets-are-embeddings f
                             (f-is-left-cancellable no-max)
                             X-is-set

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

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

    f'-is-equiv : Β¬ has-maximal-element-strong β†’ is-equiv f'
    f'-is-equiv no-max = corestriction-of-embedding-is-equivalence f
                          (f-is-embedding no-max)

    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 lem

    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 : Β¬ has-maximal-element-strong β†’ X'' ≃ Ordinal 𝓀
    e no-max = X''       β‰ƒβŸ¨ NatΞ£ Ο„ , NatΞ£-is-equiv C B Ο„ Ο„-is-equiv ⟩
        X'        β‰ƒβŸ¨ ≃-sym (f' , f'-is-equiv no-max) ⟩
        Ordinal 𝓀 β– 

    the-type-of-ordinals-is-small : Β¬ has-maximal-element-strong
                                  β†’ is-small (Ordinal 𝓀)
    the-type-of-ordinals-is-small no-max = X'' , (e no-max)

    absurd : Β¬ has-maximal-element-strong β†’ 𝟘
    absurd no-max = the-type-of-ordinals-is-large
                     (the-type-of-ordinals-is-small no-max)

axiom-of-choice-implies-zorns-lemma
 : Axiom-of-Choice
 β†’ poset-axioms (_β‰ͺ_)
 β†’ all-chains-have-upper-bound
 β†’ has-maximal-element

axiom-of-choice-implies-zorns-lemma ac (X-is-set , axioms-rest) = III
 where
  em : Excluded-Middle
  em = Choice-gives-Excluded-Middle pe' ac

  lifted-cf
   : βˆ₯ Lift (𝓀 βŠ” 𝓣) X βˆ₯
   β†’ βˆƒ Ξ΅ κž‰ (π“Ÿ (Lift (𝓀 βŠ” 𝓣) X) β†’ (Lift (𝓀 βŠ” 𝓣) X))
         , ((A : π“Ÿ (Lift (𝓀 βŠ” 𝓣) X)) β†’ is-inhabited A β†’ Ξ΅ A ∈ A)
  lifted-cf =
   Choice-gives-Choiceβ‚„ ac (Lift (𝓀 βŠ” 𝓣) X) (Lift-is-set (𝓀 βŠ” 𝓣) X X-is-set)

  lower-cf
   : Ξ£ Ξ΅ κž‰ (π“Ÿ (Lift (𝓀 βŠ” 𝓣) X) β†’ (Lift (𝓀 βŠ” 𝓣) X))
         , ((A : π“Ÿ (Lift (𝓀 βŠ” 𝓣) X)) β†’ is-inhabited A β†’ Ξ΅ A ∈ A)
   β†’  Ξ£ Ξ΅ κž‰ (π“Ÿ X β†’ X) , ((A : π“Ÿ X) β†’ is-inhabited A β†’ Ξ΅ A ∈ A)
  lower-cf (Ο΅ , f) = (Ο΅' , f')
   where
    Ο΅' : π“Ÿ X β†’ X
    ϡ' S = lower (ϡ (S ∘ lower))
    inhab-trans : {A' : π“Ÿ X} β†’ is-inhabited A' β†’ is-inhabited (A' ∘ lower)
    inhab-trans {A'} isA' =
     isA' >>= Ξ» isA'' β†’
      ∣ lift (𝓀 βŠ” 𝓣) (pr₁ isA'') ,
      transport (Ξ» q β†’ (A' q) holds) (Ξ΅-Lift (𝓀 βŠ” 𝓣) (pr₁ isA'')) (prβ‚‚ isA'')∣
    f' : (A' : π“Ÿ X) β†’ is-inhabited A' β†’ Ο΅' A' ∈ A'
    f' A' A'-inhab = (f (A' ∘ lower) (inhab-trans {A'} A'-inhab))

  choice-function : βˆ₯ X βˆ₯
                  β†’ βˆƒ Ξ΅ κž‰ (π“Ÿ X β†’ X) , ((A : π“Ÿ X) β†’ is-inhabited A β†’ Ξ΅ A ∈ A)
  choice-function isX =  βˆ₯βˆ₯-functor
                          lower-cf
                          (lifted-cf (βˆ₯βˆ₯-functor (lift (𝓀 βŠ” 𝓣)) isX))

  I' : all-chains-have-upper-bound
     β†’ βˆƒ Ξ΅ κž‰ (π“Ÿ X β†’ X) , ((A : π“Ÿ X) β†’ is-inhabited A β†’ Ξ΅ A ∈ A)
     β†’ has-maximal-element
  I' chains = βˆ₯βˆ₯-rec
               (βˆƒ-is-prop)
               (choice-function-gives-zorns-lemma em
                 (X-is-set , axioms-rest)
                 chains)

  I : all-chains-have-upper-bound β†’ βˆ₯ X βˆ₯ β†’ has-maximal-element
  I chains-have-ub z = I' chains-have-ub (choice-function z)

  empty-has-no-ub : Β¬ βˆ₯ X βˆ₯ β†’ Β¬ (all-chains-have-upper-bound {π“₯})
  empty-has-no-ub Ξ½  chains =
   Ξ½ ∣ pr₁ (chains βˆ… Ξ» x y xin yin β†’  unique-from-𝟘 (Ξ½ ∣ x ∣)) ∣

  II : all-chains-have-upper-bound  β†’  Β¬ βˆ₯ X βˆ₯ β†’ has-maximal-element
  II chains-have-ub ν = unique-from-𝟘 ((empty-has-no-ub ν) chains-have-ub)

  III : all-chains-have-upper-bound β†’ has-maximal-element
  III chains-have-ub =
   cases (I chains-have-ub) (II chains-have-ub) (em βˆ₯ X βˆ₯ βˆ₯βˆ₯-is-prop)

\end{code}