{----------------- trivia -----------------------------}
nat = data { $0, $S (n : nat) } : Set, 
zero = $0 : nat, 
succ (n : nat) = $S n : nat, 
{- plus2(n:nat) = [] : nat, -}

fun( A : Set,  B : Set)  = (x : A) -> B : Set, 
FUN( A : Type, B : Type) = (x : A) -> B : Type, 

op( A : Set) = fun A A : Set,
OP( A : Type) = FUN A A : Type,

iterate( A : Set, f : op A, x : A, n : nat) = 
 case n of {
   $0    -> x, 
   $S n1 -> f (iterate A f x n1) }
 : A, 

ITERATE (A : Type, f : OP A, x : A, n : nat) = 
 case n of {
   $0    -> x, 
   $S n1 -> f (ITERATE A f x n1)}
 : A, 

seq (A : Set) = fun nat A : Set, 
limop (A : Set) = fun (seq A) A : Set, 
                                                        
{--------------- limit structures ----------------------}

Lim = sig {
        X : Set,        {- base set -}
        x : X,          {- zero -}
        s : op X,       {- successor -}
        lim : limop X   {- limit -}
        } : Type, 

{- There is a natural (countable) product operation 
   on limit structures, defined pointwise. -}
prodLim (F :  FUN nat Lim) =
  struct { X = (n : nat) -> (F n).X, 
           x = \ n -> (F n).x, 
           s = \ u n -> (F n).s (u n), 
           lim = \ f n -> (F n).lim (\ k -> f k n) }
  : Lim, 

{- using only the limit operation, we can iterate
   an operation on the base set omega times -}
omegaIt (S : Lim, f : op (S.X) )
        = \x -> S.lim (iterate (S.X) f x)
        : op (S.X),

{- Replacing the successor operation by something
   more powerful -}
nextLim (S : Lim, f : op (S.X) ) =
  let {
     g = omegaIt S f : op (S.X)
  } in struct {
     X = S.X, 
     x = g (S.x),       {- is this right? Maybe f (S.x) ? -}
     s = g, 
     lim = S.lim
  } : Lim, 

{- an inverse limit of some kind .. -}
invLim (G : FUN nat Lim,
        F : (n : nat) -> fun ((G (succ n)).X) ((G n).X)) =
  nextLim (prodLim G) 
          ( \ s n -> F n (s (succ n))) 
  : Lim, 

{--------------------- les choses ------------------------}

{- A thing is a function T on limit structures, together
   with a `projection' function from the base set of T S 
   to the base set of S. An example follows immediately. -}
Thing = sig {  
        T : OP Lim, 
        p : (S : Lim) -> fun ((T S).X) (S.X)
        } : Type, 

{- The example of a thing -}
zeroThing =
 struct { T = \ S -> 
                struct {
                  X = op (S.X), 
                  x = S.s,        {- successor -> zero -}
                  s = omegaIt S,  {- new successor     -}
                  lim = \ f x -> S.lim (\ k -> f k x)  
                                  {- limit is `lifted', pointwise -}
                }, 
          p = \ S f -> f (S.x) 
        } : Thing,

{- a `successor' operation on things -}
nextThing (t : Thing) = 
  let { 
    T = t.T : OP Lim, 
    p = t.p : (S : Lim) -> fun ((T S).X) (S.X), 

    G (S : Lim) = ITERATE Lim T S : FUN nat Lim,      

    F (S : Lim, n : nat) = p (G S n) : fun ((G S (succ n)).X) ((G S n).X), 

    H (S : Lim) = invLim (G S) (F S) : Lim, 

    h (S : Lim) = \ u -> u zero : fun ((H S).X) (S.X)
  } in struct { T = H,  p = h } : Thing,

limThing( F : FUN nat Thing) 
        = struct {
            T = \S   -> prodLim (\k -> (F k).T S),
            p = \S f -> S.lim   (\k -> (F k).p S (f k))
        } : Thing



,
comp (t1 : Thing, t2 : Thing) 
  = struct {
     T=\x->t2.T (t1.T x),
     p=\S->\x->t1.p S (t2.p (t1.T S) x) 
    }       : Thing
{-
 struct { T = \ S -> t2.T (t1.T S), 
          p = \ S x -> t1.p S (t2.p (t1.T S) x) }
 : Thing, 
-}