Martin Escardo, 18 January 2021.

\begin{code}

{-# OPTIONS --safe --without-K --lossy-unification #-}

open import UF.Univalence

module Ordinals.ArithmeticProperties
       (ua : Univalence)
       where

open import UF.Base
open import UF.Embeddings hiding (⌊_βŒ‹)
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.ClassicalLogic
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt

private
 fe : FunExt
 fe = Univalence-gives-FunExt ua

 fe' : Fun-Ext
 fe' {𝓀} {π“₯} = fe 𝓀 π“₯

 pe : PropExt
 pe = Univalence-gives-PropExt ua

open import MLTT.Plus-Properties
open import MLTT.Spartan
open import Notation.CanonicalMap
open import Ordinals.Arithmetic fe
open import Ordinals.ConvergentSequence ua
open import Ordinals.Equivalence
open import Ordinals.Maps
open import Ordinals.Notions
open import Ordinals.OrdinalOfOrdinals ua
open import Ordinals.Type
open import Ordinals.Underlying

πŸ˜β‚’-left-neutral : (Ξ± : Ordinal 𝓀) β†’ πŸ˜β‚’ +β‚’ Ξ± = Ξ±
πŸ˜β‚’-left-neutral {𝓀} Ξ± = eqtoidβ‚’ (ua 𝓀) fe' (πŸ˜β‚’ +β‚’ Ξ±) Ξ± h
 where
  f : 𝟘 + ⟨ Ξ± ⟩ β†’ ⟨ Ξ± ⟩
  f = ⌜ 𝟘-lneutral ⌝

  f-preserves-order : (x y : 𝟘 + ⟨ Ξ± ⟩) β†’ x β‰ΊβŸ¨ πŸ˜β‚’ +β‚’ Ξ± ⟩ y β†’ f x β‰ΊβŸ¨ Ξ± ⟩ f y
  f-preserves-order (inr x) (inr y) l = l

  f-reflects-order : (x y : 𝟘 + ⟨ Ξ± ⟩) β†’ f x β‰ΊβŸ¨ Ξ± ⟩ f y β†’ x β‰ΊβŸ¨ πŸ˜β‚’ +β‚’ Ξ± ⟩ y
  f-reflects-order (inr x) (inr y) l = l


  h : (πŸ˜β‚’ +β‚’ Ξ±) ≃ₒ Ξ±
  h = f , order-preserving-reflecting-equivs-are-order-equivs (πŸ˜β‚’ +β‚’ Ξ±) Ξ± f
           (⌜⌝-is-equiv 𝟘-lneutral) f-preserves-order f-reflects-order

πŸ˜β‚’-right-neutral : (Ξ± : Ordinal 𝓀) β†’ Ξ±  +β‚’ πŸ˜β‚’ = Ξ±
πŸ˜β‚’-right-neutral Ξ± = eqtoidβ‚’ (ua _) fe' (Ξ± +β‚’ πŸ˜β‚’) Ξ± h
 where
  f : ⟨ Ξ± ⟩ + 𝟘 β†’ ⟨ Ξ± ⟩
  f = ⌜ 𝟘-rneutral' ⌝

  f-preserves-order : is-order-preserving (Ξ±  +β‚’ πŸ˜β‚’) Ξ± f
  f-preserves-order (inl x) (inl y) l = l

  f-reflects-order : is-order-reflecting (Ξ±  +β‚’ πŸ˜β‚’) Ξ± f
  f-reflects-order (inl x) (inl y) l = l


  h : (Ξ± +β‚’ πŸ˜β‚’) ≃ₒ Ξ±
  h = f , order-preserving-reflecting-equivs-are-order-equivs (Ξ± +β‚’ πŸ˜β‚’) Ξ± f
           (⌜⌝-is-equiv 𝟘-rneutral') f-preserves-order f-reflects-order

+β‚’-assoc : (Ξ± Ξ² Ξ³ : Ordinal 𝓀) β†’ (Ξ±  +β‚’ Ξ²) +β‚’ Ξ³ = Ξ±  +β‚’ (Ξ² +β‚’ Ξ³)
+β‚’-assoc Ξ± Ξ² Ξ³ = eqtoidβ‚’ (ua _) fe' ((Ξ±  +β‚’ Ξ²) +β‚’ Ξ³) (Ξ±  +β‚’ (Ξ² +β‚’ Ξ³)) h
 where
  f : ⟨ (Ξ± +β‚’ Ξ²) +β‚’ Ξ³ ⟩ β†’ ⟨ Ξ± +β‚’ (Ξ² +β‚’ Ξ³) ⟩
  f = ⌜ +assoc ⌝

  f-preserves-order : is-order-preserving  ((Ξ±  +β‚’ Ξ²) +β‚’ Ξ³) (Ξ±  +β‚’ (Ξ² +β‚’ Ξ³)) f
  f-preserves-order (inl (inl x)) (inl (inl y)) l = l
  f-preserves-order (inl (inl x)) (inl (inr y)) l = l
  f-preserves-order (inl (inr x)) (inl (inr y)) l = l
  f-preserves-order (inl (inl x)) (inr y)       l = l
  f-preserves-order (inl (inr x)) (inr y)       l = l
  f-preserves-order (inr x)       (inr y)       l = l


  f-reflects-order : is-order-reflecting ((Ξ±  +β‚’ Ξ²) +β‚’ Ξ³) (Ξ±  +β‚’ (Ξ² +β‚’ Ξ³)) f
  f-reflects-order (inl (inl x)) (inl (inl y)) l = l
  f-reflects-order (inl (inl x)) (inl (inr y)) l = l
  f-reflects-order (inl (inr x)) (inl (inr y)) l = l
  f-reflects-order (inl (inl x)) (inr y)       l = l
  f-reflects-order (inl (inr x)) (inr y)       l = l
  f-reflects-order (inr x)       (inl (inl y)) l = l
  f-reflects-order (inr x)       (inl (inr y)) l = l
  f-reflects-order (inr x)       (inr y)       l = l


  h : ((Ξ±  +β‚’ Ξ²) +β‚’ Ξ³) ≃ₒ (Ξ±  +β‚’ (Ξ² +β‚’ Ξ³))
  h = f , order-preserving-reflecting-equivs-are-order-equivs
           ((Ξ±  +β‚’ Ξ²) +β‚’ Ξ³) (Ξ±  +β‚’ (Ξ² +β‚’ Ξ³))
           f (⌜⌝-is-equiv +assoc) f-preserves-order f-reflects-order

+β‚’-↓-left : {Ξ± Ξ² : Ordinal 𝓀} (a : ⟨ Ξ± ⟩)
          β†’ (Ξ± ↓ a) = ((Ξ± +β‚’ Ξ²) ↓ inl a)
+β‚’-↓-left {𝓀} {Ξ±} {Ξ²} a = h
 where
  Ξ³ = Ξ± ↓ a
  Ξ΄ = (Ξ±  +β‚’ Ξ²) ↓ inl a

  f : ⟨ Ξ³ ⟩ β†’ ⟨ Ξ΄ ⟩
  f (x , l) = inl x , l

  g :  ⟨ Ξ΄ ⟩ β†’ ⟨ Ξ³ ⟩
  g (inl x , l) = x , l

  η : g ∘ f ∼ id
  Ξ· u = refl

  Ρ : f ∘ g ∼ id
  Ξ΅ (inl x , l) = refl

  f-is-equiv : is-equiv f
  f-is-equiv = qinvs-are-equivs f (g , Ξ· , Ξ΅)

  f-is-order-preserving : is-order-preserving Ξ³ Ξ΄ f
  f-is-order-preserving (x , _) (x' , _) l = l


  g-is-order-preserving : is-order-preserving Ξ΄ Ξ³ g
  g-is-order-preserving (inl x , _) (inl x' , _) l = l

  h : γ = δ
  h = eqtoidβ‚’ (ua 𝓀) fe' Ξ³ Ξ΄
       (f , f-is-order-preserving , f-is-equiv , g-is-order-preserving)


+β‚’-↓-right : {Ξ± Ξ² : Ordinal 𝓀} (b : ⟨ Ξ² ⟩)
           β†’ (Ξ± +β‚’ (Ξ² ↓ b)) = ((Ξ± +β‚’ Ξ²) ↓ inr b)
+β‚’-↓-right {𝓀} {Ξ±} {Ξ²} b = h
 where
  Ξ³ = Ξ±  +β‚’ (Ξ² ↓ b)
  Ξ΄ = (Ξ±  +β‚’ Ξ²) ↓ inr b

  f : ⟨ Ξ³ ⟩ β†’ ⟨ Ξ΄ ⟩
  f (inl a)       = inl a , ⋆
  f (inr (y , l)) = inr y , l

  g :  ⟨ Ξ΄ ⟩ β†’ ⟨ Ξ³ ⟩
  g (inl a , ⋆) = inl a
  g (inr y , l) = inr (y , l)

  η : g ∘ f ∼ id
  Ξ· (inl a)       = refl
  Ξ· (inr (y , l)) = refl

  Ρ : f ∘ g ∼ id
  Ξ΅ (inl a , ⋆) = refl
  Ξ΅ (inr y , l) = refl

  f-is-equiv : is-equiv f
  f-is-equiv = qinvs-are-equivs f (g , Ξ· , Ξ΅)

  f-is-order-preserving : is-order-preserving Ξ³ Ξ΄ f
  f-is-order-preserving (inl _) (inl _) l = l
  f-is-order-preserving (inl _) (inr _) l = l
  f-is-order-preserving (inr _) (inr _) l = l

  g-is-order-preserving : is-order-preserving Ξ΄ Ξ³ g
  g-is-order-preserving (inl _ , _) (inl _ , _) l = l
  g-is-order-preserving (inl _ , _) (inr _ , _) l = l
  g-is-order-preserving (inr _ , _) (inr _ , _) l = l

  h : γ = δ
  h = eqtoidβ‚’ (ua 𝓀) fe' Ξ³ Ξ΄
       (f , f-is-order-preserving , f-is-equiv , g-is-order-preserving)

\end{code}

Added 7 November 2022 by Tom de Jong.

A rather special case of the above is that adding πŸ™ and then taking the initial
segment capped at inr ⋆ is the same thing as the original ordinal.

It is indeed a special case of the above because (πŸ™ ↓ ⋆) = πŸ˜β‚’ and πŸ˜β‚’ is right
neutral, but we give a direct proof instead.

\begin{code}

+β‚’-πŸ™β‚’-↓-right : (Ξ± : Ordinal 𝓀) β†’ (Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆ = Ξ±
+β‚’-πŸ™β‚’-↓-right Ξ± = eqtoidβ‚’ (ua _) fe' ((Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆) Ξ± h
 where
  f : ⟨ (Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆ ⟩ β†’ ⟨ Ξ± ⟩
  f (inl x , l) = x

  g : ⟨ Ξ± ⟩ β†’ ⟨ (Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆ ⟩
  g x = (inl x , ⋆)

  f-order-preserving : is-order-preserving ((Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆) Ξ± f
  f-order-preserving (inl x , _) (inl y , _) l = l

  f-is-equiv : is-equiv f
  f-is-equiv = qinvs-are-equivs f (g , Ξ· , Ξ΅)
   where
    η : g ∘ f ∼ id
    Ξ· (inl _ , _) = refl

    Ρ : f ∘ g ∼ id
    Ξ΅ _ = refl

  g-order-preserving : is-order-preserving Ξ± ((Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆) g
  g-order-preserving x y l = l

  h : ((Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆) ≃ₒ Ξ±
  h = f , f-order-preserving , f-is-equiv , g-order-preserving

\end{code}

End of addition.

\begin{code}

+β‚’-⊲-left : {Ξ± Ξ² : Ordinal 𝓀} (a : ⟨ Ξ± ⟩)
          β†’ (Ξ± ↓ a) ⊲ (Ξ± +β‚’ Ξ²)
+β‚’-⊲-left {𝓀} {Ξ±} {Ξ²} a = inl a , +β‚’-↓-left a

+β‚’-⊲-right : {Ξ± Ξ² : Ordinal 𝓀} (b : ⟨ Ξ² ⟩)
           β†’ (Ξ± +β‚’ (Ξ² ↓ b)) ⊲ (Ξ± +β‚’ Ξ²)
+β‚’-⊲-right {𝓀} {Ξ±} {Ξ²} b = inr b , +β‚’-↓-right {𝓀} {Ξ±} {Ξ²} b

+β‚’-increasing-on-right : {Ξ± Ξ² Ξ³ : Ordinal 𝓀}
                       β†’ Ξ² ⊲ Ξ³
                       β†’ (Ξ± +β‚’ Ξ²) ⊲ (Ξ± +β‚’ Ξ³)
+β‚’-increasing-on-right {𝓀} {Ξ±} {Ξ²} {Ξ³} (c , p) = inr c , q
 where
  q =  (Ξ± +β‚’ Ξ²)           =⟨ ap (Ξ± +β‚’_) p ⟩
       (Ξ± +β‚’ (Ξ³ ↓ c))     =⟨ +β‚’-↓-right c ⟩
       ((Ξ± +β‚’ Ξ³) ↓ inr c) ∎

+β‚’-right-monotone : (Ξ± Ξ² Ξ³ : Ordinal 𝓀)
                  β†’ Ξ² β‰Ό Ξ³
                  β†’ (Ξ± +β‚’ Ξ²) β‰Ό (Ξ± +β‚’ Ξ³)
+β‚’-right-monotone Ξ± Ξ² Ξ³ m = to-β‰Ό Ο•
 where
  l : (a : ⟨ Ξ± ⟩) β†’ ((Ξ± +β‚’ Ξ²) ↓ inl a) ⊲  (Ξ± +β‚’ Ξ³)
  l a = o
   where
    n : (Ξ±  ↓ a) ⊲ (Ξ± +β‚’ Ξ³)
    n = +β‚’-⊲-left a

    o : ((Ξ± +β‚’ Ξ²) ↓ inl a) ⊲  (Ξ± +β‚’ Ξ³)
    o = transport (_⊲ (Ξ± +β‚’ Ξ³)) (+β‚’-↓-left a) n

  r : (b : ⟨ Ξ² ⟩) β†’ ((Ξ± +β‚’ Ξ²) ↓ inr b) ⊲ (Ξ± +β‚’ Ξ³)
  r b = s
   where
    o : (Ξ² ↓ b) ⊲ Ξ³
    o = from-β‰Ό m b

    p : (Ξ± +β‚’ (Ξ² ↓ b)) ⊲ (Ξ± +β‚’ Ξ³)
    p = +β‚’-increasing-on-right o

    q : Ξ± +β‚’ (Ξ² ↓ b) = (Ξ± +β‚’ Ξ²) ↓ inr b
    q = +β‚’-↓-right b

    s : ((Ξ± +β‚’ Ξ²) ↓ inr b) ⊲ (Ξ± +β‚’ Ξ³)
    s = transport (_⊲ (Ξ±  +β‚’ Ξ³)) q p

  Ο• : (x : ⟨ Ξ± +β‚’ Ξ² ⟩) β†’ ((Ξ± +β‚’ Ξ²) ↓ x) ⊲ (Ξ± +β‚’ Ξ³)
  Ο• = dep-cases l r


\end{code}

TODO. Find better names for the following lemmas.

\begin{code}

AP-lemmaβ‚€ : {Ξ± Ξ² : Ordinal 𝓀}
          β†’ Ξ± β‰Ό (Ξ± +β‚’ Ξ²)
AP-lemmaβ‚€ {𝓀} {Ξ±} {Ξ²} = to-β‰Ό Ο•
 where
  Ο• : (a : ⟨ Ξ± ⟩) β†’ Ξ£ z κž‰ ⟨ Ξ± +β‚’ Ξ² ⟩ , (Ξ± ↓ a) = ((Ξ± +β‚’ Ξ²) ↓ z)
  Ο• a = inl a , (+β‚’-↓-left a)

AP-lemma₁ : {Ξ± Ξ² : Ordinal 𝓀}
            (a : ⟨ α ⟩)
          β†’ (Ξ± +β‚’ Ξ²) β‰  (Ξ± ↓ a)
AP-lemma₁ {𝓀} {Ξ±} {Ξ²} a p = irrefl (OO 𝓀) (Ξ± +β‚’ Ξ²) m
 where
  l : (Ξ± +β‚’ Ξ²) ⊲ Ξ±
  l = (a , p)

  m : (Ξ± +β‚’ Ξ²) ⊲ (Ξ± +β‚’ Ξ²)
  m = AP-lemmaβ‚€ (Ξ± +β‚’ Ξ²) l

AP-lemmaβ‚‚ : {Ξ± Ξ² : Ordinal 𝓀} (a : ⟨ Ξ± ⟩)
          β†’ Ξ± = Ξ²
          β†’ Ξ£ b κž‰ ⟨ Ξ² ⟩ , (Ξ± ↓ a) = (Ξ² ↓ b)
AP-lemmaβ‚‚ a refl = a , refl

AP-lemma₃ : {Ξ± Ξ² Ξ³ : Ordinal 𝓀} (b : ⟨ Ξ² ⟩) (z : ⟨ Ξ± +β‚’ Ξ³ ⟩)
          β†’ ((Ξ± +β‚’ Ξ²) ↓ inr b) = ((Ξ± +β‚’ Ξ³) ↓ z)
          β†’ Ξ£ c κž‰ ⟨ Ξ³ ⟩ , z = inr c
AP-lemma₃ {𝓀} {Ξ±} {Ξ²} {Ξ³} b (inl a) p = 𝟘-elim (AP-lemma₁ a q)
 where
  q : (Ξ± +β‚’ (Ξ² ↓ b)) = (Ξ± ↓ a)
  q = +β‚’-↓-right b βˆ™ p βˆ™ (+β‚’-↓-left a)⁻¹

AP-lemma₃ b (inr c) p = c , refl

+β‚’-left-cancellable : (Ξ± Ξ² Ξ³ : Ordinal 𝓀)
                    β†’ (Ξ± +β‚’ Ξ²) = (Ξ± +β‚’ Ξ³)
                    β†’ Ξ² = Ξ³
+β‚’-left-cancellable {𝓀} Ξ± = g
 where
  P : Ordinal 𝓀 β†’ 𝓀 ⁺ Μ‡
  P Ξ² = βˆ€ Ξ³ β†’ (Ξ± +β‚’ Ξ²) = (Ξ± +β‚’ Ξ³) β†’ Ξ² = Ξ³

  Ο• : βˆ€ Ξ²
    β†’ (βˆ€ b β†’ P (Ξ² ↓ b))
    β†’ P Ξ²
  Ο• Ξ² f Ξ³ p = Extensionality (OO 𝓀) Ξ² Ξ³ (to-β‰Ό u) (to-β‰Ό v)
   where
    u : (b : ⟨ Ξ² ⟩) β†’ (Ξ² ↓ b) ⊲ Ξ³
    u b = c , t
     where
      z : ⟨ Ξ± +β‚’ Ξ³ ⟩
      z = pr₁ (AP-lemmaβ‚‚ (inr b) p)

      r : ((Ξ± +β‚’ Ξ²) ↓ inr b) = ((Ξ± +β‚’ Ξ³) ↓ z)
      r = prβ‚‚ (AP-lemmaβ‚‚ (inr b) p)

      c : ⟨ γ ⟩
      c = pr₁ (AP-lemma₃ b z r)

      s : z = inr c
      s = prβ‚‚ (AP-lemma₃ b z r)

      q = (Ξ± +β‚’ (Ξ² ↓ b))     =⟨ +β‚’-↓-right b ⟩
          ((Ξ± +β‚’ Ξ²) ↓ inr b) =⟨ r ⟩
          ((Ξ± +β‚’ Ξ³) ↓ z)     =⟨ ap ((Ξ± +β‚’ Ξ³) ↓_) s ⟩
          ((Ξ± +β‚’ Ξ³) ↓ inr c) =⟨ (+β‚’-↓-right c)⁻¹ ⟩
          (Ξ± +β‚’ (Ξ³ ↓ c))     ∎

      t : (Ξ² ↓ b) = (Ξ³ ↓ c)
      t = f b (Ξ³ ↓ c) q

    v : (c : ⟨ Ξ³ ⟩) β†’ (Ξ³ ↓ c) ⊲ Ξ²
    v c = b , (t ⁻¹)
     where
      z : ⟨ Ξ± +β‚’ Ξ² ⟩
      z = pr₁ (AP-lemmaβ‚‚ (inr c) (p ⁻¹))

      r : ((Ξ± +β‚’ Ξ³) ↓ inr c) = ((Ξ± +β‚’ Ξ²) ↓ z)
      r = prβ‚‚ (AP-lemmaβ‚‚ (inr c) (p ⁻¹))

      b : ⟨ β ⟩
      b = pr₁ (AP-lemma₃ c z r)

      s : z = inr b
      s = prβ‚‚ (AP-lemma₃ c z r)

      q = (Ξ± +β‚’ (Ξ³ ↓ c))     =⟨ +β‚’-↓-right c ⟩
          ((Ξ± +β‚’ Ξ³) ↓ inr c) =⟨ r ⟩
          ((Ξ± +β‚’ Ξ²) ↓ z)     =⟨ ap ((Ξ± +β‚’ Ξ²) ↓_) s ⟩
          ((Ξ± +β‚’ Ξ²) ↓ inr b) =⟨ (+β‚’-↓-right b)⁻¹ ⟩
          (Ξ± +β‚’ (Ξ² ↓ b))     ∎

      t : (Ξ² ↓ b) = (Ξ³ ↓ c)
      t = f b (Ξ³ ↓ c) (q ⁻¹)

  g : (Ξ² : Ordinal 𝓀) β†’ P Ξ²
  g = transfinite-induction-on-OO P Ο•


left-+β‚’-is-embedding : (Ξ± : Ordinal 𝓀) β†’ is-embedding (Ξ± +β‚’_)
left-+β‚’-is-embedding Ξ± = lc-maps-into-sets-are-embeddings (Ξ± +β‚’_)
                           (Ξ» {Ξ²} {Ξ³} β†’ +β‚’-left-cancellable Ξ± Ξ² Ξ³)
                           (the-type-of-ordinals-is-a-set (ua _) fe')
\end{code}

This implies that the function Ξ± +β‚’_ reflects the _⊲_ ordering:

\begin{code}

+β‚’-left-reflects-⊲ : (Ξ± Ξ² Ξ³ : Ordinal 𝓀)
                   β†’ (Ξ± +β‚’ Ξ²) ⊲ (Ξ± +β‚’ Ξ³)
                   β†’ Ξ² ⊲ Ξ³
+β‚’-left-reflects-⊲ Ξ± Ξ² Ξ³ (inl a , p) = 𝟘-elim (AP-lemma₁ a q)
   where
    q : (Ξ± +β‚’ Ξ²) = (Ξ± ↓ a)
    q = p βˆ™ (+β‚’-↓-left a)⁻¹

+β‚’-left-reflects-⊲ Ξ± Ξ² Ξ³ (inr c , p) = l
   where
    q : (Ξ± +β‚’ Ξ²) = (Ξ± +β‚’ (Ξ³ ↓ c))
    q = p βˆ™ (+β‚’-↓-right c)⁻¹

    r : Ξ² = (Ξ³ ↓ c)
    r = +β‚’-left-cancellable Ξ± Ξ² (Ξ³ ↓ c) q

    l : β ⊲ γ
    l = c , r

\end{code}

And in turn this implies that the function Ξ± +β‚’_ reflects the _β‰Ό_
partial ordering:

\begin{code}

+β‚’-left-reflects-β‰Ό : (Ξ± Ξ² Ξ³ : Ordinal 𝓀)
                   β†’ (Ξ± +β‚’ Ξ²) β‰Ό (Ξ± +β‚’ Ξ³)
                   β†’ Ξ² β‰Ό Ξ³
+β‚’-left-reflects-β‰Ό {𝓀} Ξ± Ξ² Ξ³ l = to-β‰Ό (Ο• Ξ² l)
 where
  Ο• : (Ξ² : Ordinal 𝓀)
    β†’ (Ξ± +β‚’ Ξ²) β‰Ό (Ξ± +β‚’ Ξ³)
    β†’ (b : ⟨ Ξ² ⟩) β†’ (Ξ² ↓ b) ⊲ Ξ³
  Ο• Ξ² l b = o
   where
    m : (Ξ± +β‚’ (Ξ² ↓ b)) ⊲ (Ξ± +β‚’ Ξ²)
    m = +β‚’-⊲-right b

    n : (Ξ± +β‚’ (Ξ² ↓ b)) ⊲ (Ξ± +β‚’ Ξ³)
    n = l (Ξ± +β‚’ (Ξ² ↓ b)) m

    o : (Ξ² ↓ b) ⊲ Ξ³
    o = +β‚’-left-reflects-⊲ Ξ± (Ξ² ↓ b) Ξ³ n

\end{code}

Classically, if Ξ± β‰Ό Ξ² then there is (a necessarily unique) Ξ³ with
Ξ± +β‚’ Ξ³ = Ξ². But this not necessarily the case constructively. For
that purpose, we first characterize the order of subsingleton
ordinals.

\begin{code}

module _ {𝓀 : Universe}
         (P Q : 𝓀 Μ‡ )
         (P-is-prop : is-prop P)
         (Q-is-prop : is-prop Q)
       where

 private
   p q : Ordinal 𝓀
   p = prop-ordinal P P-is-prop
   q = prop-ordinal Q Q-is-prop

 factβ‚€ : p ⊲ q β†’ Β¬ P Γ— Q
 factβ‚€ (y , r) = u , y
  where
   s : P = (Q Γ— 𝟘)
   s = ap ⟨_⟩ r

   u : Β¬ P
   u p = 𝟘-elim (prβ‚‚ (⌜ idtoeq P (Q Γ— 𝟘) s ⌝ p))

 factβ‚€-converse : Β¬ P Γ— Q β†’ p ⊲ q
 factβ‚€-converse (u , y) = (y , g)
  where
   r : P = Q Γ— 𝟘
   r = univalence-gives-propext (ua 𝓀)
        P-is-prop
        Γ—-𝟘-is-prop
        (Ξ» p β†’ 𝟘-elim (u p))
        (Ξ» (q , z) β†’ 𝟘-elim z)

   g : p = (q ↓ y)
   g = to-Σ-= (r ,
       to-Ξ£-= (dfunext fe' (Ξ» (y , z) β†’ 𝟘-elim z) ,
               being-well-order-is-prop (underlying-order (q ↓ y)) fe _ _))

 fact₁ : p β‰Ό q β†’ (P β†’ Q)
 fact₁ l x = pr₁ (from-β‰Ό {𝓀} {p} {q} l x)

 fact₁-converse : (P β†’ Q) β†’ p β‰Ό q
 fact₁-converse f = to-β‰Ό {𝓀} {p} {q} Ο•
  where
   r : P Γ— 𝟘 = Q Γ— 𝟘
   r = univalence-gives-propext (ua 𝓀)
        Γ—-𝟘-is-prop
        Γ—-𝟘-is-prop
        (Ξ» (p , z) β†’ 𝟘-elim z)
        (Ξ» (q , z) β†’ 𝟘-elim z)

   Ο• : (x : ⟨ p ⟩) β†’ (p ↓ x) ⊲ q
   Ο• x = f x , s
    where
     s : ((P Γ— 𝟘) , (Ξ» x x' β†’ 𝟘) , _) = ((Q Γ— 𝟘) , (Ξ» y y' β†’ 𝟘) , _)
     s = to-Σ-= (r ,
         to-Ξ£-= (dfunext fe' (Ξ» z β†’ 𝟘-elim (prβ‚‚ z)) ,
                 being-well-order-is-prop (underlying-order (q ↓ f x)) fe _ _))
\end{code}

The existence of ordinal subtraction implies excluded middle.

\begin{code}

existence-of-subtraction : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
existence-of-subtraction 𝓀 = (Ξ± Ξ² : Ordinal 𝓀)
                           β†’ Ξ± β‰Ό Ξ²
                           β†’ Ξ£ Ξ³ κž‰ Ordinal 𝓀 , Ξ± +β‚’ Ξ³ = Ξ²

existence-of-subtraction-is-prop : is-prop (existence-of-subtraction 𝓀)
existence-of-subtraction-is-prop = Π₃-is-prop fe'
                                    (Ξ» Ξ± Ξ² l β†’ left-+β‚’-is-embedding Ξ± Ξ²)

ordinal-subtraction-gives-excluded-middle : existence-of-subtraction 𝓀 β†’ EM 𝓀
ordinal-subtraction-gives-excluded-middle {𝓀} Ο• P P-is-prop = g
 where
  Ξ± = prop-ordinal P P-is-prop
  Ξ² = prop-ordinal πŸ™ πŸ™-is-prop
  Οƒ = Ο• Ξ± Ξ² (fact₁-converse {𝓀} P πŸ™ P-is-prop πŸ™-is-prop (Ξ» _ β†’ ⋆))

  Ξ³ : Ordinal 𝓀
  Ξ³ = pr₁ Οƒ

  r : Ξ± +β‚’ Ξ³ = Ξ²
  r = prβ‚‚ Οƒ

  s : P + ⟨ Ξ³ ⟩ = πŸ™
  s = ap ⟨_⟩ r

  t : P + ⟨ γ ⟩
  t = idtofun πŸ™ (P + ⟨ Ξ³ ⟩) (s ⁻¹) ⋆

  f : ⟨ Ξ³ ⟩ β†’ Β¬ P
  f c p = z
   where
    A : 𝓀 Μ‡ β†’ 𝓀 Μ‡
    A X = Ξ£ x κž‰ X , Ξ£ y κž‰ X , x β‰  y

    u : A (P + ⟨ γ ⟩)
    u = inl p , inr c , +disjoint

    v : Β¬ A πŸ™
    v (x , y , d) = d (πŸ™-is-prop x y)

    w : A (P + ⟨ Ξ³ ⟩) β†’ A πŸ™
    w = transport A s

    z : 𝟘
    z = v (w u)

  g : P + Β¬ P
  g = Cases t inl (Ξ» c β†’ inr (f c))

\end{code}

TODO. Another example where subtraction doesn't necessarily exist is
the situation (Ο‰ +β‚’ πŸ™β‚’) β‰Ό β„•βˆžβ‚’, discussed in the module
OrdinalOfOrdinals. The types Ο‰ +β‚’ πŸ™β‚’ and β„•βˆžβ‚’ are equal if and only if
LPO holds. Without assuming LPO, the image of the inclusion (Ο‰ +β‚’ πŸ™β‚’)
β†’ β„•βˆžβ‚’, has empty complement, and so there is nothing that can be added
to (Ο‰ +β‚’ πŸ™β‚’) to get β„•βˆžβ‚’, unless LPO holds.

\begin{code}

open import UF.Retracts
open import UF.SubtypeClassifier

retract-Ξ©-of-Ordinal : retract (Ξ© 𝓀) of (Ordinal 𝓀)
retract-Ξ©-of-Ordinal {𝓀} = r , s , Ξ·
 where
  s : Ξ© 𝓀 β†’ Ordinal 𝓀
  s (P , i) = prop-ordinal P i

  r : Ordinal 𝓀 β†’ Ξ© 𝓀
  r Ξ± = has-least Ξ± , having-least-is-prop fe' Ξ±

  η : r ∘ s ∼ id
  Ξ· (P , i) = to-subtype-= (Ξ» _ β†’ being-prop-is-prop fe') t
   where
    f : P β†’ has-least (prop-ordinal P i)
    f p = p , (Ξ» x u β†’ id)

    g : has-least (prop-ordinal P i) β†’ P
    g (p , _) = p

    t : has-least (prop-ordinal P i) = P
    t = pe 𝓀 (having-least-is-prop fe' (prop-ordinal P i)) i g f

\end{code}

Added 29 March 2022.

It is not the case in general that Ξ² β‰Ό Ξ± +β‚’ Ξ². We work with the
equivalent order _⊴_.

\begin{code}

module _ {𝓀 : Universe} where

 open import Ordinals.OrdinalOfTruthValues fe 𝓀 (pe 𝓀)

 open import UF.DiscreteAndSeparated

 ⊴-add-taboo : Ξ©β‚’ ⊴ (πŸ™β‚’ +β‚’ Ξ©β‚’) β†’ WEM 𝓀
 ⊴-add-taboo (f , s) = V
  where
   I : is-least (πŸ™β‚’ +β‚’ Ξ©β‚’) (inl ⋆)
   I (inl ⋆) u       l = l
   I (inr x) (inl ⋆) l = 𝟘-elim l
   I (inr x) (inr y) l = 𝟘-elim l

   II : f βŠ₯ = inl ⋆
   II = simulations-preserve-least Ξ©β‚’ (πŸ™β‚’ +β‚’ Ξ©β‚’) βŠ₯ (inl ⋆) f s βŠ₯-is-least I

   III : is-isolated (f βŠ₯)
   III = transport⁻¹ is-isolated II (inl-is-isolated ⋆ (πŸ™-is-discrete ⋆))

   IV : is-isolated βŠ₯
   IV = lc-maps-reflect-isolatedness f (simulations-are-lc Ξ©β‚’ (πŸ™β‚’ +β‚’ Ξ©β‚’) f s) βŠ₯ III

   V : βˆ€ P β†’ is-prop P β†’ Β¬ P + ¬¬ P
   V P i = Cases (IV (P , i))
            (Ξ» (e : βŠ₯ = (P , i))
                  β†’ inl (equal-𝟘-is-empty (ap pr₁ (e ⁻¹))))
            (Ξ» (Ξ½ : βŠ₯ β‰  (P , i))
                  β†’ inr (contrapositive
                          (Ξ» (u : Β¬ P)
                                β†’ to-subtype-= (Ξ» _ β†’ being-prop-is-prop fe')
                                   (empty-types-are-=-𝟘 fe' (pe 𝓀) u)⁻¹) Ξ½))
\end{code}

Added 4th April 2022.

\begin{code}

πŸ˜β‚’-least-⊴ : (Ξ± : Ordinal 𝓀) β†’ πŸ˜β‚’ {𝓀} ⊴ Ξ±
πŸ˜β‚’-least-⊴ Ξ± = unique-from-𝟘 , (Ξ» x y l β†’ 𝟘-elim x) , (Ξ» x y l β†’ 𝟘-elim x)

πŸ˜β‚’-least : (Ξ± : Ordinal 𝓀) β†’ πŸ˜β‚’ {𝓀} β‰Ό Ξ±
πŸ˜β‚’-least Ξ± = ⊴-gives-β‰Ό πŸ˜β‚’ Ξ± (πŸ˜β‚’-least-⊴ Ξ±)

\end{code}

Added 5th April 2022.

Successor reflects order:

\begin{code}

succβ‚’-reflects-⊴ : (Ξ± : Ordinal 𝓀) (Ξ² : Ordinal π“₯) β†’ (Ξ± +β‚’ πŸ™β‚’) ⊴ (Ξ² +β‚’ πŸ™β‚’) β†’ Ξ± ⊴ Ξ²
succβ‚’-reflects-⊴ Ξ± Ξ² (f , i , p) = g , j , q
 where
  k : (x : ⟨ Ξ± ⟩) (t : ⟨ Ξ² ⟩ + πŸ™) β†’ f (inl x) = t β†’ Ξ£ y κž‰ ⟨ Ξ² ⟩ , f (inl x) = inl y
  k x (inl y) e = y , e
  k x (inr ⋆) e = 𝟘-elim (III (f (inr ⋆)) II)
   where
    I : f (inl x) β‰ΊβŸ¨ Ξ² +β‚’ πŸ™β‚’ ⟩ (f (inr ⋆))
    I = p (inl x) (inr ⋆) ⋆

    II : inr ⋆ β‰ΊβŸ¨ Ξ² +β‚’ πŸ™β‚’ ⟩ (f (inr ⋆))
    II = transport (Ξ» - β†’ - β‰ΊβŸ¨ Ξ² +β‚’ πŸ™β‚’ ⟩ (f (inr ⋆))) e I

    III : (t : ⟨ Ξ² ⟩ + πŸ™) β†’ Β¬ (inr ⋆  β‰ΊβŸ¨ Ξ² +β‚’ πŸ™β‚’ ⟩ t)
    III (inl y) l = 𝟘-elim l
    III (inr ⋆) l = 𝟘-elim l

  h : (x : ⟨ Ξ± ⟩) β†’ Ξ£ y κž‰ ⟨ Ξ² ⟩ , f (inl x) = inl y
  h x = k x (f (inl x)) refl

  g : ⟨ Ξ± ⟩ β†’ ⟨ Ξ² ⟩
  g x = pr₁ (h x)

  Ο• : (x : ⟨ Ξ± ⟩) β†’ f (inl x) = inl (g x)
  Ο• x = prβ‚‚ (h x)

  j : is-initial-segment Ξ± Ξ² g
  j x y l = II I
   where
    m : inl y β‰ΊβŸ¨ Ξ² +β‚’ πŸ™β‚’ ⟩ f (inl x)
    m = transport⁻¹ (Ξ» - β†’ inl y β‰ΊβŸ¨ Ξ² +β‚’ πŸ™β‚’ ⟩ -) (Ο• x) l

    I : Ξ£ z κž‰ ⟨ Ξ± +β‚’ πŸ™β‚’ ⟩ , (z β‰ΊβŸ¨ Ξ± +β‚’ πŸ™β‚’ ⟩ inl x) Γ— (f z = inl y)
    I = i (inl x) (inl y) m

    II : type-of I β†’ Ξ£ x' κž‰ ⟨ Ξ± ⟩ , (x' β‰ΊβŸ¨ Ξ± ⟩ x) Γ— (g x' = y)
    II (inl x' , n , e) = x' , n , inl-lc (inl (g x') =⟨ (Ο• x')⁻¹ ⟩
                                           f (inl x') =⟨ e ⟩
                                           inl y      ∎)

  q : is-order-preserving Ξ± Ξ² g
  q x x' l = transportβ‚‚ (Ξ» y y' β†’ y β‰ΊβŸ¨ Ξ² +β‚’ πŸ™β‚’ ⟩ y') (Ο• x) (Ο• x') I
   where
    I : f (inl x) β‰ΊβŸ¨ Ξ² +β‚’ πŸ™β‚’ ⟩ f (inl x')
    I = p (inl x) (inl x') l

succβ‚’-reflects-β‰Ό : (Ξ± Ξ² : Ordinal 𝓀) β†’ (Ξ± +β‚’ πŸ™β‚’) β‰Ό (Ξ² +β‚’ πŸ™β‚’) β†’ Ξ± β‰Ό Ξ²
succβ‚’-reflects-β‰Ό Ξ± Ξ² l = ⊴-gives-β‰Ό Ξ± Ξ²
                          (succβ‚’-reflects-⊴ Ξ± Ξ²
                            (β‰Ό-gives-⊴ (Ξ± +β‚’ πŸ™β‚’) (Ξ² +β‚’ πŸ™β‚’) l))

succβ‚’-preserves-β‰Ύ : (Ξ± Ξ² : Ordinal 𝓀) β†’ Ξ± β‰Ύ Ξ² β†’ (Ξ± +β‚’ πŸ™β‚’) β‰Ύ (Ξ² +β‚’ πŸ™β‚’)
succβ‚’-preserves-β‰Ύ Ξ± Ξ² = contrapositive (succβ‚’-reflects-β‰Ό Ξ² Ξ±)

\end{code}

TODO. Actually (Ξ± +β‚’ πŸ™β‚’) ⊴ (Ξ² +β‚’ πŸ™β‚’) is equivalent to
Ξ± ≃ₒ Ξ² or Ξ² ≃ₒ Ξ± +β‚’ πŸ™β‚’ + Ξ³ for some (necessarily unique) Ξ³.
This condition in turn implies α ⊴ β (and is equivalent to α ⊴ β under
excluded middle).

However, the successor function does not preserve _⊴_ in general:

\begin{code}

succ-not-necessarily-monotone : ((Ξ± Ξ² : Ordinal 𝓀)
                                      β†’ Ξ± ⊴ Ξ²
                                      β†’ (Ξ± +β‚’ πŸ™β‚’) ⊴ (Ξ² +β‚’ πŸ™β‚’))
                              β†’ WEM 𝓀
succ-not-necessarily-monotone {𝓀} Ο• P isp = II I
 where
  Ξ± : Ordinal 𝓀
  Ξ± = prop-ordinal P isp

  I :  (Ξ± +β‚’ πŸ™β‚’) ⊴ πŸšβ‚’
  I = Ο• Ξ± πŸ™β‚’ l
   where
    l : Ξ± ⊴ πŸ™β‚’
    l = unique-to-πŸ™ ,
        (Ξ» x y (l : y β‰ΊβŸ¨ πŸ™β‚’ ⟩ ⋆) β†’ 𝟘-elim l) ,
        (Ξ» x y l β†’ l)

  II : type-of I β†’ Β¬ P + ¬¬ P
  II (f , f-is-initial , f-is-order-preserving) = III (f (inr ⋆)) refl
   where
    III : (y : ⟨ πŸšβ‚’ ⟩) β†’ f (inr ⋆) = y β†’ Β¬ P + ¬¬ P
    III (inl ⋆) e = inl VII
     where
      IV : (p : P) β†’ f (inl p) β‰ΊβŸ¨ πŸšβ‚’ ⟩ f (inr ⋆)
      IV p = f-is-order-preserving (inl p) (inr ⋆) ⋆

      V : (p : P) β†’ f (inl p) β‰ΊβŸ¨ πŸšβ‚’ ⟩ inl ⋆
      V p = transport (Ξ» - β†’ f (inl p) β‰ΊβŸ¨ πŸšβ‚’ ⟩ -) e (IV p)

      VI : (z : ⟨ πŸšβ‚’ ⟩) β†’ Β¬ (z β‰ΊβŸ¨ πŸšβ‚’ ⟩ inl ⋆)
      VI (inl ⋆) l = 𝟘-elim l
      VI (inr ⋆) l = 𝟘-elim l

      VII : Β¬ P
      VII p = VI (f (inl p)) (V p)
    III (inr ⋆) e = inr IX
     where
      VIII : Ξ£ x' κž‰ ⟨ Ξ± +β‚’ πŸ™β‚’ ⟩ , (x' β‰ΊβŸ¨ Ξ± +β‚’ πŸ™β‚’ ⟩ inr ⋆) Γ— (f x' = inl ⋆)
      VIII = f-is-initial (inr ⋆) (inl ⋆) (transport⁻¹ (Ξ» - β†’ inl ⋆ β‰ΊβŸ¨ πŸšβ‚’ ⟩ -) e ⋆)

      IX : ¬¬ P
      IX u = XI
       where
        X : βˆ€ x' β†’ Β¬ (x' β‰ΊβŸ¨ Ξ± +β‚’ πŸ™β‚’ ⟩ inr ⋆)
        X (inl p) l = u p
        X (inr ⋆) l = 𝟘-elim l

        XI : 𝟘
        XI = X (pr₁ VIII) (pr₁ (prβ‚‚ VIII))

\end{code}

TODO. Also the implication Ξ± ⊲ Ξ² β†’ (Ξ± +β‚’ πŸ™β‚’) ⊲ (Ξ² +β‚’ πŸ™β‚’) fails in general.

\begin{code}

succ-monotone : EM (𝓀 ⁺) β†’ (Ξ± Ξ² : Ordinal 𝓀) β†’ Ξ± ⊴ Ξ² β†’ (Ξ± +β‚’ πŸ™β‚’) ⊴ (Ξ² +β‚’ πŸ™β‚’)
succ-monotone em Ξ± Ξ² l = II I
 where
  I : ((Ξ± +β‚’ πŸ™β‚’) ⊲ (Ξ² +β‚’ πŸ™β‚’)) + ((Ξ± +β‚’ πŸ™β‚’) = (Ξ² +β‚’ πŸ™β‚’)) + ((Ξ² +β‚’ πŸ™β‚’) ⊲ (Ξ± +β‚’ πŸ™β‚’))
  I = trichotomy _⊲_ fe' em ⊲-is-well-order (Ξ± +β‚’ πŸ™β‚’) (Ξ² +β‚’ πŸ™β‚’)

  II : type-of I β†’ (Ξ± +β‚’ πŸ™β‚’) ⊴ (Ξ² +β‚’ πŸ™β‚’)
  II (inl m)       = ⊲-gives-⊴ _ _ m
  II (inr (inl e)) = transport ((Ξ± +β‚’ πŸ™β‚’) ⊴_) e  (⊴-refl (Ξ± +β‚’ πŸ™β‚’))
  II (inr (inr m)) = transport ((Ξ± +β‚’ πŸ™β‚’) ⊴_) VI (⊴-refl (Ξ± +β‚’ πŸ™β‚’))
   where
    III : (Ξ² +β‚’ πŸ™β‚’) ⊴ (Ξ± +β‚’ πŸ™β‚’)
    III = ⊲-gives-⊴ _ _ m

    IV : β ⊴ α
    IV = succβ‚’-reflects-⊴ Ξ² Ξ± III

    V : α = β
    V = ⊴-antisym _ _ l IV

    VI : (Ξ± +β‚’ πŸ™β‚’) = (Ξ² +β‚’ πŸ™β‚’)
    VI = ap (_+β‚’ πŸ™β‚’) V

\end{code}

TODO. EM 𝓀 is sufficient, because we can work with the resized order _⊲⁻_.

Added 21st April 2022.

We say that an ordinal is a limit ordinal if it is the least upper
bound of its predecessors:

\begin{code}

is-limit-ordinal⁺ : Ordinal 𝓀 β†’ 𝓀 ⁺ Μ‡
is-limit-ordinal⁺ {𝓀} Ξ± = (Ξ² : Ordinal 𝓀)
                         β†’ ((Ξ³ : Ordinal 𝓀) β†’ Ξ³ ⊲ Ξ± β†’ Ξ³ ⊴ Ξ²)
                         β†’ Ξ± ⊴ Ξ²
\end{code}

We give an equivalent definition below.

Recall from another module [say which one] that the existence
propositional truncations and the set-replacement property are
together equivalent to the existence of small quotients. With them we
can construct suprema of families of ordinals.

\begin{code}

open import UF.PropTrunc
open import UF.Size

module _ (pt : propositional-truncations-exist)
         (sr : Set-Replacement pt)
       where

 open import Ordinals.OrdinalOfOrdinalsSuprema ua
 open suprema pt sr

\end{code}

Recall that, by definition, Ξ³ ⊲ Ξ± iff Ξ³ is of the form Ξ± ↓ x for some
x : ⟨ α ⟩. We define the "floor" of an ordinal to be the supremum of
its predecessors:

\begin{code}

 ⌊_βŒ‹ : Ordinal 𝓀 β†’ Ordinal 𝓀
 ⌊ Ξ± βŒ‹ = sup (Ξ± ↓_)

 βŒŠβŒ‹-lower-bound : (Ξ± : Ordinal 𝓀) β†’ ⌊ Ξ± βŒ‹ ⊴ Ξ±
 βŒŠβŒ‹-lower-bound Ξ± = sup-is-lower-bound-of-upper-bounds _ Ξ± (segment-⊴ Ξ±)

 is-limit-ordinal : Ordinal 𝓀 β†’ 𝓀 Μ‡
 is-limit-ordinal Ξ± = Ξ± ⊴ ⌊ Ξ± βŒ‹

 is-limit-ordinal-fact : (Ξ± : Ordinal 𝓀)
                       β†’ is-limit-ordinal Ξ±
                       ↔ Ξ± = ⌊ Ξ± βŒ‹
 is-limit-ordinal-fact Ξ± = (Ξ» β„“ β†’ ⊴-antisym _ _ β„“ (βŒŠβŒ‹-lower-bound Ξ±)) ,
                           (Ξ» p β†’ transport (Ξ± ⊴_) p (⊴-refl Ξ±))

 successor-lemma-left : (Ξ± : Ordinal 𝓀) (x : ⟨ Ξ± ⟩) β†’ ((Ξ± +β‚’ πŸ™β‚’) ↓ inl x) ⊴ Ξ±
 successor-lemma-left Ξ± x = III
    where
     I : (Ξ± ↓ x) ⊴ Ξ±
     I = segment-⊴ α x

     II : (Ξ± ↓ x) = ((Ξ± +β‚’ πŸ™β‚’) ↓ inl x)
     II = +β‚’-↓-left x

     III : ((Ξ± +β‚’ πŸ™β‚’) ↓ inl x) ⊴ Ξ±
     III = transport (_⊴ α) II I

 successor-lemma-right : (Ξ± : Ordinal 𝓀) β†’ (Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆ = Ξ±
 successor-lemma-right Ξ±  = III
  where
   I : (πŸ™β‚’ ↓ ⋆) ⊴ πŸ˜β‚’
   I = (Ξ» x β†’ 𝟘-elim (prβ‚‚ x)) , (Ξ» x β†’ 𝟘-elim (prβ‚‚ x)) , (Ξ» x β†’ 𝟘-elim (prβ‚‚ x))

   II : (πŸ™β‚’ ↓ ⋆) = πŸ˜β‚’
   II = ⊴-antisym _ _ I (πŸ˜β‚’-least-⊴ (πŸ™β‚’ ↓ ⋆))

   III : (Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆ = Ξ±
   III = (Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆ =⟨ (+β‚’-↓-right ⋆)⁻¹ ⟩
         Ξ± +β‚’ (πŸ™β‚’ ↓ ⋆) =⟨ ap (Ξ± +β‚’_) II ⟩
         Ξ± +β‚’ πŸ˜β‚’       =⟨ πŸ˜β‚’-right-neutral Ξ± ⟩
         α             ∎

 βŒŠβŒ‹-of-successor : (Ξ± : Ordinal 𝓀)
                 β†’ ⌊ Ξ± +β‚’ πŸ™β‚’ βŒ‹ ⊴ Ξ±
 βŒŠβŒ‹-of-successor Ξ± = sup-is-lower-bound-of-upper-bounds _ Ξ± h
  where
   h : (x : ⟨ Ξ± +β‚’ πŸ™β‚’ ⟩) β†’ ((Ξ± +β‚’ πŸ™β‚’) ↓ x) ⊴ Ξ±
   h (inl x) = successor-lemma-left Ξ± x
   h (inr ⋆) = transport⁻¹ (_⊴ Ξ±) (successor-lemma-right Ξ±) (⊴-refl Ξ±)

 βŒŠβŒ‹-of-successor' : (Ξ± : Ordinal 𝓀)
                  β†’ ⌊ Ξ± +β‚’ πŸ™β‚’ βŒ‹ = Ξ±
 βŒŠβŒ‹-of-successor' Ξ± = III
  where
   I : ((Ξ± +β‚’ πŸ™β‚’) ↓ inr ⋆) ⊴ ⌊ Ξ± +β‚’ πŸ™β‚’ βŒ‹
   I = sup-is-upper-bound _ (inr ⋆)

   II : Ξ± ⊴ ⌊ Ξ± +β‚’ πŸ™β‚’ βŒ‹
   II = transport (_⊴ ⌊ Ξ± +β‚’ πŸ™β‚’ βŒ‹) (successor-lemma-right Ξ±) I

   III : ⌊ Ξ± +β‚’ πŸ™β‚’ βŒ‹ = Ξ±
   III = ⊴-antisym _ _ (βŒŠβŒ‹-of-successor Ξ±) II

 successor-increasing : (Ξ± : Ordinal 𝓀) β†’ Ξ± ⊲ (Ξ± +β‚’ πŸ™β‚’)
 successor-increasing Ξ± = inr ⋆ , ((successor-lemma-right Ξ±)⁻¹)

 successors-are-not-limit-ordinals : (Ξ± : Ordinal 𝓀)
                                   β†’ Β¬ is-limit-ordinal (Ξ± +β‚’ πŸ™β‚’)
 successors-are-not-limit-ordinals Ξ± le = irrefl (OO _) Ξ± II
  where
   I : (Ξ± +β‚’ πŸ™β‚’) ⊴ Ξ±
   I = ⊴-trans (Ξ± +β‚’ πŸ™β‚’) ⌊ Ξ± +β‚’ πŸ™β‚’ βŒ‹ Ξ± le (βŒŠβŒ‹-of-successor Ξ±)

   II : α ⊲ α
   II = ⊴-gives-β‰Ό _ _ I Ξ± (successor-increasing Ξ±)

\end{code}

TODO (easy). Show that is-limit-ordinal⁺ α is logically equivalent to
is-limit-ordinal Ξ±.

\begin{code}

 βŒŠβŒ‹-monotone : (Ξ± Ξ² : Ordinal 𝓀) β†’ Ξ± ⊴ Ξ² β†’ ⌊ Ξ± βŒ‹ ⊴ ⌊ Ξ² βŒ‹
 βŒŠβŒ‹-monotone Ξ± Ξ² le = V
  where
   I : (y : ⟨ Ξ² ⟩) β†’ (Ξ² ↓ y) ⊴ ⌊ Ξ² βŒ‹
   I = sup-is-upper-bound (Ξ² ↓_)

   II : (x : ⟨ Ξ± ⟩) β†’ (Ξ± ↓ x) ⊲ Ξ²
   II x = ⊴-gives-β‰Ό _ _ le (Ξ± ↓ x) (x , refl)

   III : (x : ⟨ Ξ± ⟩) β†’ Ξ£ y κž‰ ⟨ Ξ² ⟩ , (Ξ± ↓ x) = (Ξ² ↓ y)
   III = II

   IV : (x : ⟨ Ξ± ⟩) β†’ (Ξ± ↓ x) ⊴ ⌊ Ξ² βŒ‹
   IV x = transport⁻¹ (_⊴ ⌊ Ξ² βŒ‹) (prβ‚‚ (III x)) (I (pr₁ (III x)))

   V : sup (Ξ± ↓_) ⊴ ⌊ Ξ² βŒ‹
   V = sup-is-lower-bound-of-upper-bounds (Ξ± ↓_) ⌊ Ξ² βŒ‹ IV

\end{code}

We now give an example of an ordinal which is not a limit ordinal and
also is not a successor ordinal unless LPO holds:

\begin{code}

 open import CoNaturals.Type
 open import Notation.CanonicalMap
 open import Notation.Order
 open import Naturals.Order

 βŒŠβŒ‹-of-β„•βˆž : ⌊ β„•βˆžβ‚’ βŒ‹ = Ο‰
 βŒŠβŒ‹-of-β„•βˆž = c
  where
   a : ⌊ β„•βˆžβ‚’ βŒ‹ ⊴ Ο‰
   a = sup-is-lower-bound-of-upper-bounds (β„•βˆžβ‚’ ↓_) Ο‰ I
    where
     I : (u : ⟨ β„•βˆžβ‚’ ⟩) β†’ (β„•βˆžβ‚’ ↓ u) ⊴ Ο‰
     I u = β‰Ό-gives-⊴ (β„•βˆžβ‚’ ↓ u) Ο‰ II
      where
       II : (Ξ± : Ordinal 𝓀₀) β†’ Ξ± ⊲ (β„•βˆžβ‚’ ↓ u) β†’ Ξ± ⊲ Ο‰
       II .((β„•βˆžβ‚’ ↓ u) ↓ (ΞΉ n , n , refl , p)) ((.(ΞΉ n) , n , refl , p) , refl) = XI
        where
         III : ΞΉ n β‰Ί u
         III = n , refl , p

         IV : ((β„•βˆžβ‚’ ↓ u) ↓ (ΞΉ n , n , refl , p)) = β„•βˆžβ‚’ ↓ ΞΉ n
         IV = iterated-↓ β„•βˆžβ‚’ u (ΞΉ n) III

         V : (β„•βˆžβ‚’ ↓ ΞΉ n) ≃ₒ (Ο‰ ↓ n)
         V = f , fop , qinvs-are-equivs f (g , gf , fg) , gop
          where
           f : ⟨ β„•βˆžβ‚’ ↓ ΞΉ n ⟩ β†’ ⟨ Ο‰ ↓ n ⟩
           f (.(ι k) , k , refl , q) = k , ⊏-gives-< _ _ q

           g : ⟨ Ο‰ ↓ n ⟩ β†’ ⟨ β„•βˆžβ‚’ ↓ ΞΉ n ⟩
           g (k , l) = (ι k , k , refl , <-gives-⊏ _ _ l)

           fg : f ∘ g ∼ id
           fg (k , l) = to-subtype-= (Ξ» k β†’ <-is-prop-valued k n) refl

           gf : g ∘ f ∼ id
           gf (.(ι k) , k , refl , q) = to-subtype-=
                                         (Ξ» u β†’ β‰Ί-prop-valued fe' u (ΞΉ n))
                                         refl

           fop : is-order-preserving (β„•βˆžβ‚’ ↓ ΞΉ n) (Ο‰ ↓ n) f
           fop (.(ΞΉ k) , k , refl , q) (.(ΞΉ k') , k' , refl , q') (m , r , cc) =
            VIII
            where
             VI : k = m
             VI = β„•-to-β„•βˆž-lc r

             VII : m < k'
             VII = ⊏-gives-< _ _ cc

             VIII : k < k'
             VIII = transport⁻¹ (_< k') VI VII

           gop : is-order-preserving (Ο‰ ↓ n) (β„•βˆžβ‚’ ↓ ΞΉ n)  g
           gop (k , l) (k' , l') β„“ = k , refl , <-gives-⊏ _ _ β„“

         IX : β„•βˆžβ‚’ ↓ ΞΉ n = Ο‰ ↓ n
         IX = eqtoidβ‚’ (ua 𝓀₀) fe' _ _ V

         X : (β„•βˆžβ‚’ ↓ (ΞΉ n)) ⊲ Ο‰
         X = n , IX

         XI : ((β„•βˆžβ‚’ ↓ u) ↓ (ΞΉ n , n , refl , p)) ⊲ Ο‰
         XI = transport⁻¹ (_⊲ Ο‰) IV X

   b : Ο‰ ⊴ ⌊ β„•βˆžβ‚’ βŒ‹
   b = transport (_⊴ ⌊ β„•βˆžβ‚’ βŒ‹) (βŒŠβŒ‹-of-successor' Ο‰) I
    where
     I : ⌊ Ο‰ +β‚’ πŸ™β‚’ βŒ‹ ⊴ ⌊ β„•βˆžβ‚’ βŒ‹
     I = βŒŠβŒ‹-monotone (Ο‰ +β‚’ πŸ™β‚’) β„•βˆžβ‚’ Ο‰+πŸ™-is-⊴-β„•βˆž

   c : ⌊ β„•βˆžβ‚’ βŒ‹ = Ο‰
   c = ⊴-antisym _ _ a b

 β„•βˆž-is-not-limit : Β¬ is-limit-ordinal β„•βˆžβ‚’
 β„•βˆž-is-not-limit β„“ = III II
  where
   I = β„•βˆžβ‚’     =⟨ lr-implication (is-limit-ordinal-fact β„•βˆžβ‚’) β„“ ⟩
       ⌊ β„•βˆžβ‚’ βŒ‹ =⟨ βŒŠβŒ‹-of-β„•βˆž  ⟩
       Ο‰       ∎

   II : β„•βˆžβ‚’ ≃ₒ Ο‰
   II = idtoeqβ‚’ _ _ I

   III : Β¬ (β„•βˆžβ‚’ ≃ₒ Ο‰)
   III (f , e) = irrefl Ο‰ (f ∞) VII
    where
     IV : is-largest Ο‰ (f ∞)
     IV = order-equivs-preserve-largest β„•βˆžβ‚’ Ο‰ f e ∞
           (Ξ» u t l β†’ β‰Ίβ‰Ό-gives-β‰Ί t u ∞ l (∞-largest u))

     V : f ∞ β‰ΊβŸ¨ Ο‰ ⟩ succ (f ∞)
     V = <-succ (f ∞)

     VI : succ (f ∞) β‰ΌβŸ¨ Ο‰ ⟩ f ∞
     VI = IV (succ (f ∞))

     VII : f ∞ β‰ΊβŸ¨ Ο‰ ⟩ f ∞
     VII = VI (f ∞) V

 open import Taboos.LPO fe

 β„•βˆž-successor-gives-LPO : (Ξ£ Ξ± κž‰ Ordinal 𝓀₀ , (β„•βˆžβ‚’ = (Ξ± +β‚’ πŸ™β‚’))) β†’ LPO
 β„•βˆž-successor-gives-LPO (Ξ± , p) = IV
  where
   I = Ξ±           =⟨ (βŒŠβŒ‹-of-successor' Ξ±)⁻¹ ⟩
       ⌊ Ξ± +β‚’ πŸ™β‚’ βŒ‹ =⟨ ap ⌊_βŒ‹ (p ⁻¹) ⟩
       ⌊ β„•βˆžβ‚’ βŒ‹     =⟨ βŒŠβŒ‹-of-β„•βˆž ⟩
       Ο‰           ∎

   II : β„•βˆžβ‚’ = (Ο‰ +β‚’ πŸ™β‚’)
   II = transport (Ξ» - β†’ β„•βˆžβ‚’ = (- +β‚’ πŸ™β‚’)) I p

   III : β„•βˆžβ‚’ ⊴ (Ο‰ +β‚’ πŸ™β‚’)
   III = transport (β„•βˆžβ‚’ ⊴_) II (⊴-refl β„•βˆžβ‚’)

   IV : LPO
   IV = β„•βˆž-⊴-Ο‰+πŸ™-gives-LPO III

 open PropositionalTruncation pt

 β„•βˆž-successor-gives-LPO' : (βˆƒ Ξ± κž‰ Ordinal 𝓀₀ , (β„•βˆžβ‚’ = (Ξ± +β‚’ πŸ™β‚’))) β†’ LPO
 β„•βˆž-successor-gives-LPO' = βˆ₯βˆ₯-rec LPO-is-prop β„•βˆž-successor-gives-LPO

 LPO-gives-β„•βˆž-successor : LPO β†’ (Ξ£ Ξ± κž‰ Ordinal 𝓀₀ , (β„•βˆžβ‚’ = (Ξ± +β‚’ πŸ™β‚’)))
 LPO-gives-β„•βˆž-successor lpo = Ο‰ , β„•βˆž-is-successor₃ lpo

\end{code}

Therefore, constructively, it is not necessarily the case that every
ordinal is either a successor or a limit.

TODO (1st June 2023). A classically equivalently definition of limit
ordinal Ξ± is that there is some Ξ² < Ξ±, and for evert Ξ² < Ξ± there is Ξ³
with Ξ² < Ξ³ < Ξ±. We have that β„•βˆž is a limit ordinal in this sense.

Added 4th May 2022.

\begin{code}

open import Ordinals.ToppedType fe
open import Ordinals.ToppedArithmetic fe

alternative-plusβ‚’ : (Ο„β‚€ τ₁ : Ordinalα΅€ 𝓀)
                  β†’ [ Ο„β‚€ +α΅’ τ₁ ] ≃ₒ ([ Ο„β‚€ ] +β‚’ [ τ₁ ])
alternative-plusβ‚’ Ο„β‚€ τ₁ = e
 where
  Ο… = cases (Ξ» ⋆ β†’ Ο„β‚€) (Ξ» ⋆ β†’ τ₁)

  f : ⟨ βˆ‘ πŸšα΅’ Ο… ⟩ β†’ ⟨ [ Ο„β‚€ ] +β‚’ [ τ₁ ] ⟩
  f (inl ⋆ , x) = inl x
  f (inr ⋆ , y) = inr y

  g : ⟨ [ Ο„β‚€ ] +β‚’ [ τ₁ ] ⟩ β†’ ⟨ βˆ‘ πŸšα΅’ Ο… ⟩
  g (inl x) = (inl ⋆ , x)
  g (inr y) = (inr ⋆ , y)

  η : g ∘ f ∼ id
  Ξ· (inl ⋆ , x) = refl
  Ξ· (inr ⋆ , y) = refl

  Ρ : f ∘ g ∼ id
  Ξ΅ (inl x) = refl
  Ξ΅ (inr y) = refl

  f-is-equiv : is-equiv f
  f-is-equiv = qinvs-are-equivs f (g , Ξ· , Ξ΅)
  f-is-op : is-order-preserving [ βˆ‘ πŸšα΅’ Ο… ] ([ Ο„β‚€ ] +β‚’ [ τ₁ ]) f

  f-is-op (inl ⋆ , _) (inl ⋆ , _) (inr (refl , l)) = l
  f-is-op (inl ⋆ , _) (inr ⋆ , _) (inl ⋆)          = ⋆
  f-is-op (inr ⋆ , _) (inl ⋆ , _) (inl l)          = l
  f-is-op (inr ⋆ , _) (inr ⋆ , _) (inr (refl , l)) = l

  g-is-op : is-order-preserving ([ Ο„β‚€ ] +β‚’ [ τ₁ ]) [ βˆ‘ πŸšα΅’ Ο… ] g
  g-is-op (inl _) (inl _) l = inr (refl , l)
  g-is-op (inl _) (inr _) ⋆ = inl ⋆
  g-is-op (inr _) (inl _) ()
  g-is-op (inr _) (inr _) l = inr (refl , l)

  e : [ βˆ‘ πŸšα΅’ Ο… ] ≃ₒ ([ Ο„β‚€ ] +β‚’ [ τ₁ ])
  e = f , f-is-op , f-is-equiv , g-is-op

alternative-plus : (Ο„β‚€ τ₁ : Ordinalα΅€ 𝓀)
                 β†’ [ Ο„β‚€ +α΅’ τ₁ ] = ([ Ο„β‚€ ] +β‚’ [ τ₁ ])
alternative-plus Ο„β‚€ τ₁ = eqtoidβ‚’ (ua _) fe' _ _ (alternative-plusβ‚’ Ο„β‚€ τ₁)

\end{code}