{-
\begin{verbatim}
Time-stamp: "1997-10-13 11:59:16 peter"
#include "./standard.half" 
#include "./Boole.half" 
\end{verbatim}
-}

  N3 = {- Codes for the first 3 `number-classes' -}
       data { $0, $1, $omega } 
     : Set
{-
\newcommand{\Nthree}{\ensuremath{\mathit{N3}}}
-}

, T3 =  {- decoding an element of $\Nthree$ -}
        \ n3 ->
        case n3 of 
        {     $0  -> N0   {- the empty set -}
        ,     $1  -> N1   {- `the' singleton -}
        , $omega  -> Nat  {- the natural numbers -}
        }
     : Pow N3 
{-
\newcommand{\Tthree}[1]{\ensuremath{\mathit{T3(#1)}}}
-}

, O = {- trees with 3 kinds of node - nillary, unary, countably branching. -} 
      data { $0 {- nillary -}
           , $S ( p : O ) {- unary -}
           , $L ( os : ( n : Nat )-> O ) } {- countably branching -}
    : Set 
{- 
I call the elements of the type $O$ countable tree ordinals.
-}

{- There is something unresolved below: debris -} 
, O' = {-  might these work?! -} 
      data { $0 ( os : ( n : N0 )-> O' )
           , $S ( os : ( n : N1 )-> O' )
           , $L ( os : ( n : Nat )-> O' ) } 
    : Set 

, ON {- ordinal notations for countable tree-ordinals -}
  = sig 
    { T : Set
    , cf : ( t : T )-> N3
    , pd : ( t : T
           , i : T3 (cf t) 
           )-> T
    }     
  : Type   
  
, Example1
  = {- notations for $\epsilon_0$. -}
    let { T = data 
              { $0, $W ( a : T, b : T ) } 
            : Set
        , f = \ a b n 
              -> case n of 
                 { $0  -> a
                 , $S p -> $W (f a b p) b
                 }
            : ( a : T, b : T, n : Nat )-> T
        , g = \ a b c 
              -> case c of 
                 { $0  -> f a b
                 , $W a1 b1 -> \ n -> $W a (g b a1 b1 n)
                 }
            : ( a : T, b : T, c : T, n : Nat )-> T
        } in  
        struct 
        { T = T 
        , cf = \ t 
               -> case t of 
                  { $0  -> $0
                  , $W a b 
                    -> case b of 
                       { $0  -> $1
                       , $W a1 b1 -> $omega
                       }
                  }
        , pd = \ t 
               -> case t of 
                  { $0  -> \ i -> case i of {}
                  , $W a b 
                    -> case b of 
                       { $0  -> \ i -> a
                       , $W a1 b1 -> g a a1 b1 
                       } 
                  }
        }
  : ON 

, Example2 
  = {- cheating ordinal notations: the ordinals themselves -}
    struct 
    { T  = O
    , cf = \ t
           -> case t of 
              { $0 -> $0
              , $S junk -> $1
              , $L junk -> $omega
              }
    , pd = \ t 
           -> case t of 
              { $0  -> \ i -> case i of {}
              , $S p -> \ i -> p
              , $L os -> os 
              }
    }
  : ON 

, Acc (X : ON, a : X.T )
  = data { $0 ( phi : ( i : T3 (X.cf a) )-> Acc X (X.pd a i) ) }
  : Set

{- Now some definitions that do not work .. -}

, ON2O ( X : ON, a : X.T, a' : Acc X a )
  = {- the interpretation of the accessible element a as an ordinal -}
    let { t = X.cf a : N3 } in 
    case a' of {
      $0 phi -> case t of {
                 $0  -> $0,
                 $1  -> $S (ON2O X (X.pd a [$0]) (phi [$0])),
                 $omega  -> $L (\n->ON2O X (X.pd a [n]) (phi [n]))}}
  : O

{- try to reverse the approach -} 
, ON2O ( X : ON, a : X.T, a' : Acc X a )
  = {- the interpretation of the accessible element a as an ordinal -}
    case X.cf a of 
    { $0  -> $0
    , $1  -> case a' of 
             { $0 phi -> $S (ON2O X (X.pd a [$0]) (phi [$0]))}
    , $omega  
          -> case a' of 
             { $0 phi -> $L (\n->ON2O X (X.pd a [n]) (phi [n])) }
    }
  : O

, Acc' ( X : ON, a : X.T )
  = case X.cf a of 
    { $0  -> N1
    , $1  -> Acc' X (X.pd a [$0])
    , $omega  -> ( n : Nat )-> Acc' X (X.pd a [n])
    }
  : Set

, th ( A : Set, B : ( a : A )-> Set, c : ( a : A, b : B a )-> A )
  = theory 
    { W 
      = data { $0 ( a : A, phi : ( b : B a )-> W ) } 
      : Set
    , t ( w : W ) 
      = case w of { $0 a phi -> a }
      : A
    , Acc ( a : A ) 
      = data { $0 ( phi : ( b : B a )-> Acc (c a b) ) }
      : Set
    , Acc2W ( a : A, a' : Acc a ) 
      = case a' of 
        { $0 phi -> $0 a ( \ b -> Acc2W (c a b) (phi b) ) }
      : W 
    }
  : Theory