{- Ordinals:
   Copyright (c) Groupoid Infinity, 2014-2018. -}


module ordinal where

import nat

-- from the JSL 89 paper of Stan Wainer
-- by @coquand

-- http://www.cse.chalmers.se/~coquand/ordinal.ps
data ord  = zero
          | succ (n:         ord)
          | lim  (f: nat  -> ord)

data ord2 = zero
          | succ (n:         ord2)
          | lim  (f: nat  -> ord2)
          | lim2 (f: ord  -> ord2)

data ord3 = zero
          | succ (n:         ord3)
          | lim  (f: nat  -> ord3)
          | lim2 (f: ord  -> ord3)
          | lim3 (f: ord2 -> ord3)

inj0 : nat -> ord = split
 zero -> zero
 succ n -> succ (inj0 n)

inj12 : ord -> ord2 = split
 zero -> zero
 succ z -> succ (inj12 z)
 lim f -> lim (\ (n:nat) -> inj12 (f n))

omega : ord = lim inj0
omega1 : ord2 = lim2 inj12

G1 : ord -> nat -> nat = split
 zero -> \ (x:nat) -> zero
 succ z -> \ (x:nat) -> succ (G1 z x)
 lim f -> \ (x:nat) -> G1 (f x) x

G2 : ord2 -> nat -> ord = split
 zero -> \ (x:nat) -> zero
 succ z -> \ (x:nat) -> succ (G2 z x)
 lim f -> \ (x:nat) -> G2 (f x) x
 lim2 f -> \ (x:nat) -> lim (\ (n:nat) -> G2 (f (inj0 n)) x)

and (A B : U) : U = (_:A) * B

O2 (n:nat) : ord2 -> U = split 
 zero -> unit
 succ z -> O2 n z
 lim f -> (p:nat) -> O2 n (f p)
 lim2 f -> (x:ord) -> and (O2 n (f x)) (Path ord (G2 (f x) n) (G2 (f (inj0 (G1 x n))) n))


H1 : ord -> nat -> nat = split 
 zero -> \ (x:nat) -> x
 succ z -> \ (x:nat) -> H1 z (succ x)
 lim f -> \ (x:nat) -> H1 (f x) x

H2 : ord2 -> ord -> ord = split 
 zero -> \ (x:ord) -> x
 succ z -> \ (x:ord) -> H2 z (succ x)
 lim f -> \ (x:ord) -> lim (\ (n:nat) -> H2 (f n) x)
 lim2 f -> \ (x:ord) -> H2 (f x) x

collapsing (n:nat) : 
 (x:ord2) (y:ord) -> O2 n x -> Path nat (G1 (H2 x y) n) (H1 (G2 x n) (G1 y n)) = split
  zero -> \ (y:ord) (h:O2 n zero) -> <i>G1 y n
  succ z -> \ (y:ord) (h:O2 n (succ z)) -> collapsing n z (succ y) h
  lim f ->  \ (y:ord) (h:O2 n (lim f)) -> collapsing n (f n) y (h n)
  lim2 f -> \ (y:ord) (h:O2 n (lim2 f)) -> 
         let
           rem : Path ord (G2 (f y) n) (G2 (f (inj0 (G1 y n))) n) = (h y).2
           rem1 : Path nat (G1 (H2 (f y) y) n) (H1 (G2 (f y) n) (G1 y n)) = collapsing n (f y) y (h y).1
         in comp (<i>Path nat (G1 (H2 (f y) y) n) (H1 (rem@i) (G1 y n))) rem1 []

-- an application


lemOmega1 (n:nat) : O2 n omega1 = \ (x:ord) -> (rem x,rem1 x)
 where rem : (x:ord) -> O2 n (inj12 x) = split
         zero -> tt
         succ z -> rem z
         lim f -> \ (p:nat) -> rem (f p)
       rem1 : (x:ord) -> Path ord (G2 (inj12 x) n) (G2 (inj12 (inj0 (G1 x n))) n) = split
         zero -> <i>zero
         succ z -> <i>succ ((rem1 z)@i)
         lim f -> rem1 (f n)

corr1 (n:nat) : Path nat (G1 (H2 omega1 omega) n) (H1 (G2 omega1 n) (G1 omega n)) =
 collapsing n omega1 omega (lemOmega1 n)

lem : (n p:nat) -> Path nat (G1 (inj0 n) p) n = split
 zero -> \ (p:nat) -> <i>zero
 succ q -> \ (p:nat) -> <i> succ (lem q p@i)

lem1 (n:nat) : Path nat (G1 omega n) n = lem n n

lem2 : (n p:nat) -> Path ord (G2 (inj12 (inj0 n)) p) (inj0 n) = split
 zero -> \ (p:nat) -> <i>inj0 zero
 succ q -> \ (p:nat) -> <i> succ (lem2 q p@i)

test (n:nat) : ord = G2 omega1 n

lem3 (n:nat) : Path ord (G2 (inj12 (inj0 n)) n) (inj0 n) = lem2 n n