open import Arith::Nat using (Nat)
open import Relation::Formula

// https://choukh.github.io/agda-lvo/NonWellFormed.Ordinal.html
open data Ord
| zero | suc Ord
| lim (Nat → Ord)

open data Depth Ord
| suc α ⇒ empty
| suc α ⇒ next (Depth α)
| lim f ⇒ exist (n : Nat) (Depth (f n))

variable α β : Ord
def pred (Depth α) : Ord
| {suc α}, empty ⇒ α
| next d ⇒ pred d
| exist n d ⇒ pred d

open data infix ≤ Ord Ord
| zero, β ⇒ z≤
| suc α, β ⇒ s≤ (d : Depth β) (α ≤ pred d)
| lim f, β ⇒ l≤ (∀ n → f n ≤ β)

def ≤f⇒≤l (f : _) (n : Nat) (α ≤ f n) : α ≤ lim f
| _, _, z≤ ⇒ z≤
| _, _, s≤ _ ≤∸ ⇒ s≤ (exist {f} _ _) ≤∸
| f, n, l≤ f≤ ⇒ l≤ (\ m ⇒ ≤f⇒≤l f n (f≤ m))

def ≤∸⇒≤ {d : Depth β} (α ≤ pred d) : α ≤ β
| z≤ ⇒ z≤
| s≤ _ ≤∸ ⇒ s≤ d (≤∸⇒≤ ≤∸)
| l≤ f≤ ⇒ l≤ (\ n ⇒ ≤∸⇒≤ (f≤ n))

def ≤⇒∸≤ (d : Depth α) (α ≤ β) : pred d ≤ β
| empty, s≤ _ ≤∸ ⇒ ≤∸⇒≤ ≤∸
| next d, s≤ _ ≤∸ ⇒ ≤⇒∸≤ d (≤∸⇒≤ ≤∸)
| exist n d, l≤ f≤ ⇒ ≤⇒∸≤ d (f≤ n)

def l≤l {f g : Nat → Ord} (f≤g : ∀ n → f n ≤ g n) : lim f ≤ lim g ⇒
  // l≤ (\ n => ≤f⇒≤l _ _ (f≤g n))
  // seems to cause Aya to loop
  l≤ (\ n ⇒ ≤f⇒≤l g n (f≤g n))

def s≤s (p : α ≤ β) : suc α ≤ suc β ⇒ s≤ empty p

def ≤-refl : Reflexive (≤)
| {zero} ⇒ z≤
| {suc α} ⇒ s≤s ≤-refl
| {lim f} ⇒ l≤ (\ n ⇒ ≤f⇒≤l f n ≤-refl)

def ≤-trans : Transitive (≤)
| z≤, _ ⇒ z≤
| s≤ empty α≤β, s≤ _ β≤γ ⇒ s≤ _ (≤-trans α≤β β≤γ)
| s≤ (next d) α≤β, s≤ _ β≤γ ⇒ s≤ _ (≤-trans α≤β (≤⇒∸≤ d β≤γ))
| s≤ (exist n d) α≤β, l≤ f≤γ ⇒ ≤-trans (s≤ d α≤β) (f≤γ n)
| l≤ f≤β, β≤γ ⇒ l≤ (\ n ⇒ ≤-trans (f≤β n) β≤γ)

def s∸≤ (d : Depth α) : suc (pred d) ≤ α
| empty ⇒ ≤-refl
| next d ⇒ s≤s (≤⇒∸≤ d ≤-refl)
| exist n _ as dd ⇒ s≤ dd ≤-refl

def infix ≈ : Rel Ord ⇒ \ α β ⇒ Σ (α ≤ β) ** β ≤ α

// This implicit lambda is supposed to be omitted.
def ≈-refl : Reflexive (≈) ⇒ \ {x} ⇒ (≤-refl , ≤-refl)

def ≈-sym : Symmetric (≈)
| (p , q) ⇒ (q , p)

def ≤z⇒≈z' (α ≤ zero) : α ≈ zero
| z≤ ⇒ ≈-refl
| s≤ () _
| {lim _}, ≤ ⇒ (≤ , z≤)

def l≈l {f g : Nat → Ord} (f≈g : ∀ n → f n ≈ g n) : lim f ≈ lim g ⇒
  (l≤l (\ n ⇒ (f≈g n) .1), l≤l (\ n ⇒ (f≈g n).2))