Martin Escardo 2018.

Classically, the ordinals Ο +β πβ and βββ are equal.  Constructively,
we have (Ο +β πβ) β΄ βββ, but the inequality in the other direction is
equivalent to LPO.

\begin{code}

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

open import UF.Univalence
open import UF.FunExt
open import UF.UA-FunExt

module Ordinals.ConvergentSequence (ua : Univalence) where

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

fe' : Fun-Ext
fe' {π€} {π₯} =  fe π€ π₯

open import MLTT.Spartan
open import Notation.CanonicalMap
open import Taboos.LPO
open import Naturals.Order
open import Ordinals.Arithmetic fe
open import Ordinals.OrdinalOfOrdinals ua
open import Ordinals.Type
open import Ordinals.Equivalence
open import Ordinals.Underlying
open import CoNaturals.Type
open import UF.Equiv

Ο+π-is-β΄-ββ : (Ο +β πβ) β΄ βββ
Ο+π-is-β΄-ββ = ΞΉπ , i , p
where
i : (x : β¨ Ο +β πβ β©) (y : β¨ βββ β©)
β y βΊβ¨ βββ β© ΞΉπ x
β Ξ£ x' κ β¨ Ο +β πβ β© , (x' βΊβ¨ Ο +β πβ β© x) Γ (ΞΉπ x' οΌ y)
i (inl m) y (n , r , l) = inl n , β-gives-< n m l , (r β»ΒΉ)
i (inr *) y (n , r , l) = inl n , * , (r β»ΒΉ)

p : (x y : β¨ Ο +β πβ β©)
β x βΊβ¨ Ο +β πβ β© y
β ΞΉπ x βΊβ¨ βββ β© ΞΉπ y
p (inl n) (inl m) l = β-to-ββ-order-preserving n m l
p (inl n) (inr *) * = β-βΊ-largest n
p (inr *) (inl m) l = π-elim l
p (inr *) (inr *) l = π-elim l

ββ-β΄-Ο+π-gives-LPO : βββ β΄ (Ο +β πβ) β LPO
ββ-β΄-Ο+π-gives-LPO l = Ξ³
where
b : (Ο +β πβ) ββ βββ
b = bisimilarity-gives-ordinal-equiv (Ο +β πβ) βββ Ο+π-is-β΄-ββ l

e : is-equiv ΞΉπ
e = prβ (ββ-gives-β (Ο +β πβ) βββ b)

Ξ³ : LPO
Ξ³ = ΞΉπ-has-section-gives-LPO (equivs-have-sections ΞΉπ e)

LPO-gives-ββ-β΄-Ο+π-gives : LPO β βββ β΄ (Ο +β πβ)
LPO-gives-ββ-β΄-Ο+π-gives lpo = (Ξ» x β ΞΉπ-inverse x (lpo x)) ,
(Ξ» x β i x (lpo x)) ,
(Ξ» x y β p x y (lpo x) (lpo y))
where
ΞΉπ-inverse-inl : (u : ββ) (d : is-decidable (Ξ£ n κ β , u οΌ ΞΉ n))
β (m : β) β u οΌ ΞΉ m β ΞΉπ-inverse u d οΌ inl m
ΞΉπ-inverse-inl . (ΞΉ n) (inl (n , refl)) m q = ap inl (β-to-ββ-lc q)
ΞΉπ-inverse-inl u          (inr g)          m q = π-elim (g (m , q))

i : (x : ββ) (d : is-decidable (Ξ£ n κ β , x οΌ ΞΉ n)) (y : β + π)
β y βΊβ¨ Ο +β πβ β© ΞΉπ-inverse x d
β Ξ£ x' κ ββ , (x' βΊβ¨ βββ β© x) Γ (ΞΉπ-inverse x' (lpo x') οΌ y)
i .(ΞΉ n) (inl (n , refl)) (inl m) l =
ΞΉ m ,
β-to-ββ-order-preserving m n l ,
ΞΉπ-inverse-inl (ΞΉ m) (lpo (ΞΉ m)) m refl
i .(ΞΉ n) (inl (n , refl)) (inr *) l = π-elim l
i x (inr g) (inl n) * =
ΞΉ n ,
transport (underlying-order βββ (ΞΉ n))
((not-finite-is-β (fe π€β π€β) (curry g)) β»ΒΉ)
(β-βΊ-largest n) ,
ΞΉπ-inverse-inl (ΞΉ n) (lpo (ΞΉ n)) n refl
i x (inr g) (inr *) l = π-elim l

p : (x y : ββ)  (d : is-decidable (Ξ£ n κ β , x οΌ ΞΉ n))
(e : is-decidable (Ξ£ m κ β , y οΌ ΞΉ m))
β  x βΊβ¨ βββ β© y
β ΞΉπ-inverse x d βΊβ¨ Ο +β πβ β© ΞΉπ-inverse y e
p .(ΞΉ n) .(ΞΉ m) (inl (n , refl)) (inl (m , refl)) (k , r , l) =
transportβ»ΒΉ (Ξ» - β - <β m) (β-to-ββ-lc r) (β-gives-< k m l)
p .(ΞΉ n) y (inl (n , refl)) (inr f) l = β
p x y (inr f) e (k , r , l) =
π-elim (β-is-not-finite k ((not-finite-is-β (fe π€β π€β) (curry f))β»ΒΉ β r))

ββ-is-successorβ : LPO β βββ ββ (Ο +β πβ)
ββ-is-successorβ lpo = bisimilarity-gives-ordinal-equiv
βββ
(Ο +β πβ)
(LPO-gives-ββ-β΄-Ο+π-gives lpo)
Ο+π-is-β΄-ββ

ββ-is-successorβ : LPO β ββ β (β + π)
ββ-is-successorβ lpo = ββ-gives-β βββ (Ο +β πβ) (ββ-is-successorβ lpo)

ββ-is-successorβ : LPO β βββ οΌ (Ο +β πβ)
ββ-is-successorβ lpo = eqtoidβ (ua π€β) fe' βββ (Ο +β πβ) (ββ-is-successorβ lpo)

ββ-is-successorβ : LPO β ββ οΌ (β + π)
ββ-is-successorβ lpo = eqtoid (ua π€β) ββ (β + π) (ββ-is-successorβ lpo)

\end{code}