Martin Escardo, 18 January 2021.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline --experimental-lossy-unification #-}

open import UF-Univalence

module OrdinalArithmetic-Properties
       (ua : Univalence)
       where

open import UF-Base
open import UF-Subsingletons
open import UF-Subsingletons-FunExt
open import UF-Equiv
open import UF-UA-FunExt
open import UF-FunExt
open import UF-EquivalenceExamples
open import UF-Embeddings
open import UF-ExcludedMiddle

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

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

 pe : PropExt
 pe = Univalence-gives-PropExt ua

open import SpartanMLTT
open import OrdinalsType
open import OrdinalNotions
open import OrdinalOfOrdinals ua
open import OrdinalArithmetic fe
open import Plus-Properties

πŸ˜β‚’-left-neutral : (Ξ± : Ordinal 𝓀) β†’ πŸ˜β‚’ +β‚’ Ξ± ≑ Ξ±
πŸ˜β‚’-left-neutral Ξ± = eqtoidβ‚’ (πŸ˜β‚’ +β‚’ Ξ±) Ξ± 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β‚’ (Ξ± +β‚’ πŸ˜β‚’) Ξ± 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β‚’ ((Ξ±  +β‚’ Ξ²) +β‚’ Ξ³) (Ξ±  +β‚’ (Ξ² +β‚’ Ξ³)) 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β‚’ Ξ³ Ξ΄ (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β‚’ Ξ³ Ξ΄ (f , f-is-order-preserving , f-is-equiv , g-is-order-preserving)

+β‚’-⊲-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}

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

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

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

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

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

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₁ (lemmaβ‚‚ (inr b) p)

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

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

      s : z ≑ inr c
      s = prβ‚‚ (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₁ (lemmaβ‚‚ (inr c) (p ⁻¹))

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

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

      s : z ≑ inr b
      s = prβ‚‚ (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

\end{code}

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

\begin{code}

+β‚’-left-reflects-⊲ : (Ξ± Ξ² Ξ³ : Ordinal 𝓀)
                   β†’ (Ξ± +β‚’ Ξ²) ⊲ (Ξ± +β‚’ Ξ³)
                   β†’ Ξ² ⊲ Ξ³
+β‚’-left-reflects-⊲ Ξ± Ξ² Ξ³ (inl a , p) = 𝟘-elim (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}

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

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 OrdinalOfTruthValues fe 𝓀 (pe 𝓀)

 open import DiscreteAndSeparated
 open import UF-Miscelanea

 ⊴-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 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 gives 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 CanonicalMapNotation
 open import GenericConvergentSequence
 open import OrderNotation
 open import NaturalsOrder

 βŒŠβŒ‹-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β‚’ _ _ 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 (Ο‰ +β‚’ πŸ™β‚’) β„•βˆžβ‚’ β„•βˆž-in-Ord.fact

   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 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 = β„•βˆž-in-Ord.converse-fails-constructively 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 = Ο‰ , β„•βˆž-in-Ord.corollary₃ lpo

\end{code}

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

Added 4th May 2022.

\begin{code}

open import OrdinalsToppedType fe
open import OrdinalToppedArithmetic 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β‚’ _ _ (alternative-plusβ‚’ Ο„β‚€ τ₁)

\end{code}