Martin Escardo, 18 January 2021.

Small additions by Tom de Jong in May 2024.

\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 = β π-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 = β π-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 (x , l) = inl x , l

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 (inl a)       = inl a , β
f (inr (y , l)) = inr y , l

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)

+β-β²-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)
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 = 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 = 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}

\begin{code}

πβ-least-β΄ : (Ξ± : Ordinal π€) β πβ {π€} β΄ Ξ±
πβ-least-β΄ Ξ± = unique-from-π , (Ξ» x y l β π-elim x) , (Ξ» x y l β π-elim x)

πβ-least : (Ξ± : Ordinal π€) β πβ {π€} βΌ Ξ±
πβ-least Ξ± = β΄-gives-βΌ πβ Ξ± (πβ-least-β΄ Ξ±)

\end{code}

Originally added 21st April 2022 by MartΓ­n EscardΓ³.
Moved up here on 27th May 2024 by Tom de Jong.

\begin{code}

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 Ξ± β©
Ξ±                 β

successor-increasing : (Ξ± : Ordinal π€) β Ξ± β² (Ξ± +β πβ)
successor-increasing Ξ± = inr β , ((successor-lemma-right Ξ±)β»ΒΉ)

\end{code}

Added on 24th May 2024 by Tom de Jong.

\begin{code}

upper-bound-of-successors-of-initial-segments :
(Ξ± : Ordinal π€) (a : β¨ Ξ± β©) β ((Ξ± β a) +β πβ) β΄ Ξ±
upper-bound-of-successors-of-initial-segments Ξ± a = to-β΄ ((Ξ± β a) +β πβ) Ξ± I
where
I : (x : β¨ (Ξ± β a) +β πβ β©) β (((Ξ± β a) +β πβ) β x) β² Ξ±
I (inl (b , l)) = b , (((Ξ± β a) +β πβ) β inl (b , l) οΌβ¨ eβ β©
(Ξ± β a) β (b , l)             οΌβ¨ eβ β©
Ξ± β b                         β)
where
eβ = (+β-β-left (b , l)) β»ΒΉ
eβ = iterated-β Ξ± a b l
I (inr β) = a , successor-lemma-right (Ξ± β a)

\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 Γ π)

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 + β¨ Ξ³ β© οΌ π

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 {π€} = 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}

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

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 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 _β²β»_.

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 the modules UF.Quotients.FromSetReplacement and
UF.Quotients.GivesSetReplacement 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 Ξ±))

ββ-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

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.

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

Added 24th May 2024 by Tom de Jong.

Every ordinal is the supremum of the successors of its initial segments.

\begin{code}

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

open import Ordinals.OrdinalOfOrdinalsSuprema ua
open suprema pt sr

supremum-of-successors-of-initial-segments :
(Ξ± : Ordinal π€) β Ξ± οΌ sup (Ξ» x β (Ξ± β x) +β πβ)
supremum-of-successors-of-initial-segments {π€} Ξ± =
Antisymmetry (OO π€) Ξ± s (to-βΌ I) (β΄-gives-βΌ s Ξ± II)
where
s : Ordinal π€
s = sup (Ξ» x β (Ξ± β x) +β πβ)
F : β¨ Ξ± β© β Ordinal π€
F x = (Ξ± β x) +β πβ

I : (a : β¨ Ξ± β©) β (Ξ± β a) β² s
I a = f (inr β) , ((Ξ± β a)         οΌβ¨ eβ β©
(F a β inr β)   οΌβ¨ eβ β©
(s β f (inr β)) β)
where
f : (y : β¨ F a β©) β β¨ s β©
f = [ F a , s ]β¨ sup-is-upper-bound F a β©
eβ = (successor-lemma-right (Ξ± β a)) β»ΒΉ
eβ = (initial-segment-of-sup-at-component F a (inr β)) β»ΒΉ

II : s β΄ Ξ±
II = sup-is-lower-bound-of-upper-bounds F Ξ±
(upper-bound-of-successors-of-initial-segments Ξ±)

\end{code}

Added 2 June 2024 by Tom de Jong.

\begin{code}

no-greatest-ordinal : Β¬ (Ξ£ Ξ± κ Ordinal π€ , ((Ξ² : Ordinal π€) β Ξ² β΄ Ξ±))
no-greatest-ordinal {π€} (Ξ± , Ξ±-greatest) = irrefl (OO π€) Ξ± IV
where
I : (Ξ± +β πβ) β΄ Ξ±
I = Ξ±-greatest (Ξ± +β πβ)
II : Ξ± β΄ (Ξ± +β πβ)
II = β²-gives-β΄ Ξ± (Ξ± +β πβ) (successor-increasing Ξ±)
III : Ξ± +β πβ οΌ Ξ±
III = β΄-antisym (Ξ± +β πβ) Ξ± I II
IV : Ξ± β² Ξ±
IV = transport (Ξ± β²_) III (successor-increasing Ξ±)

\end{code}