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