{-# OPTIONS --allow-unsolved-metas #-}
open import Level
module ordinal where

open import zf

open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 

open import  Relation.Binary.PropositionalEquality

data OrdinalD {n : Level} :  (lv : Nat) → Set n where
   Φ : (lv : Nat) → OrdinalD  lv
   OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
   ℵ_ :  (lv : Nat) → OrdinalD (Suc lv)

record Ordinal {n : Level} : Set n where
   field
     lv : Nat
     ord : OrdinalD {n} lv

data ¬ℵ  {n : Level} {lx : Nat } : ( x : OrdinalD {n} lx ) → Set where
    ¬ℵΦ : ¬ℵ (Φ lx) 
    ¬ℵs : {x : OrdinalD {n} lx } → ¬ℵ x → ¬ℵ (OSuc lx x) 

data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
   Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
   s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
   ℵΦ< : {lx : Nat} → Φ  (Suc lx) d< (ℵ lx) 
   ℵ<  : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → ¬ℵ x  →  OSuc  (Suc lx) x d< (ℵ lx) 
   ℵs< : {lx : Nat} → (ℵ lx) d< OSuc (Suc lx) (ℵ lx)
   ℵss< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → (ℵ lx) d< x → (ℵ lx) d< OSuc (Suc lx) x 

open Ordinal

_o<_ : {n : Level} ( x y : Ordinal ) → Set n
_o<_ x y =  (lv x < lv y )  ∨ ( ord x d< ord y )

o<-subst : {n : Level } {Z X z x : Ordinal {n}}  → Z o< X → Z ≡ z  →  X ≡ x  →  z o< x
o<-subst df refl refl = df

open import Data.Nat.Properties 
open import Data.Empty
open import Data.Unit using ( ⊤ )
open import Relation.Nullary

open import Relation.Binary
open import Relation.Binary.Core

o∅ : {n : Level} → Ordinal {n}
o∅  = record { lv = Zero ; ord = Φ Zero }

s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
s<refl {n} {lv} {Φ lv}  = Φ<
s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
s<refl {n} {Suc lv} {ℵ lv} = ℵs<

open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)

ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
      lv x  ≡ lv y → ord x ≅ ord y →  x ≡ y
ordinal-cong refl refl = refl

≡→¬d< : {n : Level} →  {lv : Nat} → {x  : OrdinalD {n}  lv }  → x d< x → ⊥
≡→¬d<  {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t

trio<> : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  →  y d< x → x d< y → ⊥
trio<>  {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) = trio<> s t
trio<> {_} {.(Suc _)} {.(OSuc (Suc _) (ℵ _))} {.(ℵ _)} ℵs< (ℵ< {_} {.(ℵ _)} ())
trio<> {_} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} (ℵ< ()) ℵs<
trio<> {n} {lx} {.(OSuc lx _)} {.(Φ lx)} Φ< ()
trio<> {n} {.(Suc _)} {.(ℵ _)} {.(Φ (Suc _))} ℵΦ< ()
trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (Φ (Suc _)))} (ℵ< ¬ℵΦ) (ℵss< ())
trio<> {n} {.(Suc _)} {.(ℵ _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} (ℵ< (¬ℵs x)) (ℵss< x<y) = trio<> (ℵ< x) x<y
trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (Φ (Suc _)))} {.(ℵ _)} (ℵss< ()) (ℵ< ¬ℵΦ)
trio<> {n} {.(Suc _)} {.(OSuc (Suc _) (OSuc (Suc _) _))} {.(ℵ _)} (ℵss< y<x) (ℵ< (¬ℵs x)) = trio<> y<x (ℵ< x)

trio<≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → x d< y → ⊥
trio<≡ refl = ≡→¬d<

trio>≡ : {n : Level} →  {lx : Nat} {x  : OrdinalD {n} lx } { y : OrdinalD  lx }  → x ≡ y  → y d< x → ⊥
trio>≡ refl = ≡→¬d<

triO : {n : Level} →  {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
triO  {n} {lx} {ly} x y = <-cmp lx ly

fin : {n : Level} →  {lx : Nat} → {y : OrdinalD {n} (Suc lx) } → y d< (ℵ lx) → ¬ℵ y
fin {_} {_} {Φ (Suc _)} ℵΦ< = ¬ℵΦ
fin {_} {_} {OSuc (Suc _) _} (ℵ< x) = ¬ℵs x

triOrdd : {n : Level} →  {lx : Nat}   → Trichotomous  _≡_ ( _d<_  {n} {lx} {lx} )
triOrdd  {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
triOrdd  {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
triOrdd  {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
triOrdd  {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri<  ℵΦ<  (λ ()) ( λ lt → trio<> lt ℵΦ<) 
triOrdd  {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt ℵΦ< ) (λ ()) ℵΦ<  
triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y ) with triOrdd (ℵ lv) y
triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri< a ¬b ¬c = tri< (ℵss< a) (λ ()) (trio<> (ℵss< a) )
triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri≈ ¬a refl ¬c = tri<  ℵs< (λ ()) ( λ lt → trio<> lt  ℵs< )
triOrdd {_} {Suc lv} (ℵ lv) (OSuc .(Suc lv) y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt ( ℵ< (fin c))  ) (λ ()) ( ℵ< (fin c) )
triOrdd  {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
triOrdd  {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) with triOrdd x (ℵ lv)
triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri< a ¬b ¬c = tri< (ℵ< (fin a ) ) (λ ()) (  λ lt → trio<> lt (ℵ< (fin a ))) 
triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri≈ ¬a refl ¬c = tri> (λ lt → trio<> lt ℵs< ) (λ ()) ℵs< 
triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) | tri> ¬a ¬b c = tri> (λ lt → trio<> lt (ℵss< c  )) (λ ()) ( ℵss< c  )
triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) )  (  λ lt → trio<> lt (s< a) )
triOrdd  {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
triOrdd  {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> (  λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)

d<→lv : {n : Level} {x y  : Ordinal {n}}   → ord x d< ord y → lv x ≡ lv y
d<→lv Φ< = refl
d<→lv (s< lt) = refl
d<→lv ℵΦ< = refl
d<→lv (ℵ< _) = refl
d<→lv ℵs< = refl
d<→lv (ℵss< _) = refl

xsyℵ :  {n : Level} {lx : Nat} {x y : OrdinalD {n}  lx }   → x d< y → ¬ℵ y → ¬ℵ x
xsyℵ {_} {_} {Φ lv₁} {y} x<y t = ¬ℵΦ
xsyℵ {_} {_} {OSuc lv₁ x} {OSuc lv₁ y} (s< x<y) (¬ℵs t) = ¬ℵs ( xsyℵ x<y t)
xsyℵ {_} {_} {OSuc .(Suc _) x} {.(ℵ _)} (ℵ< x₁) ()
xsyℵ {_} {_} {ℵ lv₁} {.(OSuc (Suc lv₁) (ℵ lv₁))} ℵs< (¬ℵs t) = t
xsyℵ (ℵss< ()) (¬ℵs ¬ℵΦ)
xsyℵ (ℵss< x<y) (¬ℵs t) = xsyℵ x<y t

orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n}  lx }   → x d< y → y d< z → x d< z
orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ< 
orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< (ℵ< _) = ℵΦ< 
orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) (Φ (Suc lx)))} {.(ℵ lx)} (s< ()) (ℵ< ¬ℵΦ)
orddtrans ℵs< (ℵ< ())
orddtrans {n} {Suc lx} {OSuc (Suc lx) x} {OSuc (Suc ly) y} {ℵ _} (s< x<y) (ℵ< t) = ℵ< ( xsyℵ x<y t )
orddtrans {n} {.(Suc _)} {.(Φ (Suc _))} {.(ℵ _)} {.(OSuc (Suc _) (ℵ _))} ℵΦ< ℵs< = Φ<
orddtrans {n} {.(Suc _)} {OSuc (Suc _) .(Φ (Suc _))} {.(ℵ _)} {OSuc (Suc _) (ℵ k)} (ℵ< ¬ℵΦ) ℵs< = s<  ℵΦ< 
orddtrans {n} {.(Suc _)} {OSuc (Suc lv) (OSuc (Suc _) x)} {ℵ lv} {.(OSuc (Suc _) (ℵ _))} (ℵ< (¬ℵs t)) ℵs< = s< ( ℵ< t )
orddtrans {n} {.(Suc lv)} {ℵ lv} {OSuc .(Suc lv) (ℵ lv)} {OSuc .(Suc lv) .(OSuc (Suc lv) (ℵ lv))} ℵs< (s< ℵs<) = ℵss< ℵs<
orddtrans ℵΦ< (ℵss< y<z) = Φ<
orddtrans (ℵ< {lx} {Φ .(Suc lx)} nxx) (ℵss< {_} {k} y<z) = s< (orddtrans ℵΦ<   y<z)
orddtrans (ℵ< {lx} {OSuc .(Suc lx) xx} (¬ℵs nxx)) (ℵss< y<z) = s< (orddtrans (ℵ< nxx) y<z) 
orddtrans (ℵ< {.lv₁} {ℵ lv₁} ()) (ℵss< y<z) 
orddtrans (ℵss< x<y) (s< y<z) = ℵss< ( orddtrans x<y y<z )
orddtrans (ℵss< ()) (ℵ< ¬ℵΦ)
orddtrans (ℵss< ℵs<) (ℵ< (¬ℵs ()))
orddtrans (ℵss< (ℵss< x<y)) (ℵ< (¬ℵs x)) = orddtrans (ℵss< x<y) ( ℵ< x )
orddtrans {n} {Suc lx} {x} {y} {z} ℵs< (s< (ℵss< {lx} {ss} y<z)) = ℵss< ( ℵss< y<z )

max : (x y : Nat) → Nat
max Zero Zero = Zero
max Zero (Suc x) = (Suc x)
max (Suc x) Zero = (Suc x)
max (Suc x) (Suc y) = Suc ( max x y )

maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx  →  OrdinalD  lx  →  OrdinalD  lx
maxαd x y with triOrdd x y
maxαd x y | tri< a ¬b ¬c = y
maxαd x y | tri≈ ¬a b ¬c = x
maxαd x y | tri> ¬a ¬b c = x

maxα : {n : Level} →  Ordinal {n} →  Ordinal  → Ordinal
maxα x y with <-cmp (lv x) (lv y)
maxα x y | tri< a ¬b ¬c = x
maxα x y | tri> ¬a ¬b c = y
maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }

_o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
a o≤ b  = (a ≡ b)  ∨ ( a o< b )

ordtrans : {n : Level} {x y z : Ordinal {n} }   → x o< y → y o< z → x o< z
ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
... | refl = case1 x₁
ordtrans {n} {x} {y} {z} (case2 x₁) (case1 x₂) with d<→lv x₁
... | refl = case1 x₂
ordtrans {n} {x} {y} {z} (case2 x₁) (case2 x₂) with d<→lv x₁ | d<→lv x₂
... | refl | refl = case2 ( orddtrans x₁ x₂ )


trio< : {n : Level } → Trichotomous {suc n} _≡_  _o<_ 
trio< a b with <-cmp (lv a) (lv b)
trio< a b | tri< a₁ ¬b ¬c = tri< (case1  a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
   lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
   lemma1 (case1 x) = ¬c x
   lemma1 (case2 x) with d<→lv x
   lemma1 (case2 x) | refl = ¬b refl
trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
   lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
   lemma1 (case1 x) = ¬a x
   lemma1 (case2 x) with d<→lv x
   lemma1 (case2 x) | refl = ¬b refl
trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
   lemma1 refl = refl
   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x)
   lemma2 (case1 x) = ¬a x
   lemma2 (case2 x) = trio<> x a
trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where
   lemma1 :  (record { lv = _ ; ord = x }) ≡ b →  x ≡ ord b
   lemma1 refl = refl
   lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
   lemma2 (case1 x) = ¬a x
   lemma2 (case2 x) = trio<> x c
trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
   lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
   lemma1 (case1 x) = ¬a x
   lemma1 (case2 x) = ≡→¬d< x

OrdTrans : {n : Level} → Transitive {suc n} _o≤_
OrdTrans (case1 refl) (case1 refl) = case1 refl
OrdTrans (case1 refl) (case2 lt2) = case2 lt2
OrdTrans (case2 lt1) (case1 refl) = case2 lt1
OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x )
OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x
OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y)
OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y
OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y ))

OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
OrdPreorder {n} = record { Carrier = Ordinal
   ; _≈_  = _≡_ 
   ; _∼_   = _o≤_
   ; isPreorder   = record {
        isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
        ; reflexive     = case1 
        ; trans         = OrdTrans 
     }
 }

TransFinite : {n : Level} → { ψ : Ordinal {n} → Set n }
  → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 
  → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
  → ( ∀ (lx : Nat ) → (x : OrdinalD lx )  → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
  →  ∀ (x : Ordinal)  → ψ x
TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
TransFinite caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
    ( TransFinite caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
TransFinite caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁