{-# OPTIONS --allow-unsolved-metas #-}

{-
  0, 1, 2, 3, 4, ..., ω, ω + 1, ω + 2, ...,
  ^^^^^^^^^^^^^^^^^^  ^
   these are natural   ∞ is not a nat. numb.
       numbers

  ω + ω = ω·2, ..., ω·3, ..., ω·ω = ω², ..., ω³, ...,

  ω^ω, ..., ω^(ω·2), ..., ω^(ω^ω), ..., ω^(ω^(ω^ω)), ...,

  ω^(ω^(ω^…)) = ε₀, ε₀ + 1, ..., ε₀·2, ...,

  ε₀^(ε₀^(ε₀^…)) = ε₁, ..., ε₂, ..., ε_ω, ..., ε_{ω+1}, ...,

  ε_{ε₀}, ..., ε_{ε₁}, ..., ε_{ε₂}, ..., ε_{ε_{ε_…}} = ζ₀, ...

  This is the beginning of the list of ordinal numbers.
  The displayed numbers are still tiny in the sense that
  each number has only countably many predeccesors.
-}

{-
  Picture of ω:
    :-)   I  I  I  I  I  ...
    
  Picture of ω + 1:
         +------------------+ 
    :-)  |I  I  I  I  I  ...|  I
         +------------------+
        
  Picture of ω + ω + 1:
         +-------------+  +-------------+
    :-)  |I  I  I  ... |  |I  I  I  ... |  I
         +-------------+  +-------------+

  Picture of 1 + ω:
    :-)   I  I  I  I  I  I  ...

  What do we know about ω + 1 vs. 1 + ω?
  A: succ ω = ω + 1 > ω;   1 + ω = ω.
-}

{-
  The three fundamental convictions regarding (countable)
  ordinals numbers are:

  1. Zero should exist.
  2. Every number should have a successor.
  3. Every (strictly ascending) sequence should have a limit.

  For instance, ω is the limit of the sequence
    0,   1,   2,  3, ...
    ||   ||   ||
    f 0  f 1  f 2

  Note: ω is also the limit of the sequence
    0,   1,   2,   4,   8,  16,  32, ...
    ||   ||   ||   ||   ||
    g 0  g 1  g 2  g 3  g 4
-}

data  : Set where
  zer : 
  suc :   

-- The type "Monotonic f" is the type of witnesses
-- that "f" is a strictly increasing sequence.
data O : Set
Monotonic : (  O)  Set
_<_ : O  O  Set
data _≤_ : O  O  Set

Monotonic f = (n : )  f n < f (suc n)

-- O is not precisely the type of ordinals,
-- but the type of representations of ordinals.
-- Many ordinals have more than one representation.
data O where
  zero : O
  succ : O  O
  lim  : (f :   O)  Monotonic f  O

x < y = succ x  y

data _≤_ where
  ≤-zero     : {x : O}  zero  x
  ≤-succ-mon : {x y : O}  x  y  succ x  succ y
  ≤-trans    : {x y z : O}  x  y  y  z  x  z
  ≤-cocone   : {f :   O} {fmon : Monotonic f} {x : O} {n : }
              x  f n  x  lim f fmon
  ≤-limiting : {f :   O} {fmon : Monotonic f} {x : O}
              ((n : )  f n  x)  lim f fmon  x

fromℕ :   O
fromℕ zer     = zero
fromℕ (suc n) = succ (fromℕ n)

fromℕ-monotonic : Monotonic fromℕ
fromℕ-monotonic = {!!}

ω : O
ω = lim fromℕ fromℕ-monotonic
-- "ω is the limit of the sequence 0, 1, 2, ..."

ω' : O
ω' = lim  n  fromℕ (suc n)) {!!}
-- "ω' is the limit of the sequence 1, 2, 3, ..."

data  : Set where
_≡_ = {!!}

example₀ : ω  ω'  
example₀ = {!!}

example₁ : ω  ω'
example₁ = {!!}

example₂ : ω'  ω
example₂ = {!!}

_+_ : O  O  O
x + zero       = x
x + succ y     = succ (x + y)
x + lim f fmon = lim  n  x + f n) {!!}

example₃ : ω < succ ω
example₃ = {!!}

example₄ : (succ zero + ω)  ω
example₄ = {!!}