diff --git a/TTTAS.cabal b/TTTAS.cabal
--- a/TTTAS.cabal
+++ b/TTTAS.cabal
@@ -1,7 +1,7 @@
-cabal-version:      >=1.2
+cabal-version:      >=1.2.3
 build-type:         Simple
 name:               TTTAS
-version:            0.2.1
+version:            0.3.0
 license:            LGPL
 license-file:       COPYRIGHT
 maintainer:         Arthur Baars <abaars@iti.upv.es>
@@ -11,7 +11,7 @@
 category: 
 stability:          Stable
 copyright:          Universiteit Utrecht
-build-depends:      base, haskell98
+build-depends:      base >= 2 && < 4.1.0.0, haskell98
 exposed-modules:    Language.TTTAS       
 extensions:         Arrows, GADTs, CPP
 hs-source-dirs:     src
diff --git a/examples/CSE2.hs b/examples/CSE2.hs
--- a/examples/CSE2.hs
+++ b/examples/CSE2.hs
@@ -69,7 +69,7 @@
          case newERef1 e
          of Trafo2 step -> step (MapExpr1 m)
        Just r   -> TrafoE2 (MapExpr1 m) 
-                        (\e (T t) env1 ->  (t r, T t, env1))
+                        (\e (T t) env1 upds ->  (t r, T t, env1, upds))
     )
 
   newERef1 ::  Expr1 a 
@@ -79,10 +79,11 @@
     (\(MapExpr1 m :: MapExpr1 env1) ->
        let m2 = MapExpr1  (\s -> aux1 (matchExpr1 e s) m s)
        in TrafoE2  m2 
-                 (\e (T t) env1 -> (  t Zero
-                                   ,  T (t . Suc) 
-                                   ,  Ext env1 e
-    )            )                 )
+                 (\e (T t) env1 upds ->  (  t Zero
+                                         ,  T (t . Suc) 
+                                         ,  Ext env1 e
+                                         ,  upds
+    )            )                       )
 
   aux1 :: Maybe (Equal a x) -> (Expr1 x -> Maybe (Ref x env1)) 
        -> Expr1 x -> Maybe (Ref x (env1,a))
@@ -202,7 +203,7 @@
          case newERef e
          of Trafo2 step -> step (MapExpr m)
        Just r   -> TrafoE2 (MapExpr m) 
-                        (\e (T t) env1 ->  (t r, T t, env1))
+                        (\e (T t) env1 upds ->  (t r, T t, env1, upds))
     )
 
   newERef ::  Expr a env
@@ -212,10 +213,11 @@
     (\(MapExpr m :: MapExpr env env1) ->
        let m2 = MapExpr (\s -> aux (matchExpr e s) m s)
        in TrafoE2  m2 
-                 (\e (T t) env1 -> (  t Zero
-                                   ,  T (t . Suc) 
-                                   ,  Ext env1 e
-    )            )                 )
+                 (\e (T t) env1 upds ->  (  t Zero
+                                         ,  T (t . Suc) 
+                                         ,  Ext env1 e
+                                         ,  upds
+    )            )                       )
 
   aux :: Maybe (Equal a x) -> (Expr x env -> Maybe (Ref x env1)) 
       -> Expr x env -> Maybe (Ref x (env1,a))
diff --git a/src/Language/TTTAS.hs b/src/Language/TTTAS.hs
--- a/src/Language/TTTAS.hs
+++ b/src/Language/TTTAS.hs
@@ -31,6 +31,9 @@
                -- ** Create New References
                Unit(..),
                newSRef, extEnv, castSRef, updateSRef,
+
+               -- ** Update the Final Environment
+               updateFinalEnv,
  
                -- ** Run a Trafo
                Result(..), 
@@ -47,12 +50,17 @@
                -- ** Create New References
                newSRef2,
 
+               -- ** Update the Final Environment
+               UpdFinalEnv(..), updateFinalEnv2,
+
                -- ** Run a Trafo2 
                runTrafo2,
 
                -- ** Arrow-style Combinators
                Pair(..), Arrow2(..), ArrowLoop2(..),
+               (>>>>),
                List(..), sequenceA2
+
              ) where
  
 import Unsafe.Coerce ( unsafeCoerce )
@@ -127,6 +135,7 @@
 lookupEnv  :: Ref a env -> Env t s env -> t a s
 lookupEnv  Zero     (Ext _ t)   =  t
 lookupEnv  (Suc r)  (Ext ts _)  =  lookupEnv r ts
+lookupEnv  _        _           =  error "Error: The impossible happened!"
 
 updateEnv  ::  (t a s -> t a s) -> Ref a env 
            ->  Env t s env ->  Env t s env
@@ -134,7 +143,10 @@
               =        Ext ts (f t) 
 updateEnv  f  (Suc r)  (Ext ts t)  
               =        Ext (updateEnv f r ts)  t
+updateEnv  _  _        _ 
+              =  error "Error: The impossible happened!"
 
+
 -- | When the types @def@ and @use@ of an 'Env' coincide,
 --   we can be sure that the references in the terms do not
 --   point to values outside the environment but point
@@ -162,14 +174,19 @@
 --   the definition of 'Trafo'.  
 --   It can be seen that a 'Trafo' is a function taking as arguments: the input (@a@),
 --   a 'Ref'-transformer (@T env2 s@) from the environment constructed in this step 
---   to the final environment and the environment (@Env t s env1@) where the 
---   current transformation starts. The function returns: the output (@b@), a 
---   'Ref'-transformer (@T env1 s@) from the initial environment of this step to the final 
---   environment and the environment (@Env t s env2@) constructed in this step.
+--   to the final environment, the environment (@Env t s env1@) where the current 
+--   transformation starts and a function (@FinalEnv t s -> FinalEnv t s@) to update 
+--   (modify) the final environment. The function returns: the output (@b@), 
+--   a 'Ref'-transformer (@T env1 s@) from the initial environment of this step to the final 
+--   environment, the environment (@Env t s env2@) constructed in this step and a function 
+--   (@FinalEnv t s -> FinalEnv t s@) to update (modify) the final environment.
+--   NOTE: The function (@FinalEnv t s -> FinalEnv t s@) was introduced in version 0.3. 
+--   It's carried throw the transformation steps and can be modified (composed to another function)
+--   using the function 'updateFinalEnv'.
 data  TrafoE m t s env1 a b = 
  forall env2 . TrafoE   (  m env2)
-                        (       a  ->  T env2 s ->  Env t s env1
-                          -> (  b,     T env1 s,    Env t s env2)
+                        (       a  ->  T env2 s ->  Env t s env1 -> (FinalEnv t s -> FinalEnv t s)
+                          -> (  b,     T env1 s,    Env t s env2, (FinalEnv t s -> FinalEnv t s))
                         )
 
 data Unit s         = Unit
@@ -183,24 +200,30 @@
  =  Trafo  (\ _->  extEnv Unit)
 
 
+-- | The function 'updateFinalEnv' returns a 'Trafo' that introduces a function
+--   (@FinalEnv t s -> FinalEnv t s@) to update the final environment.
+updateFinalEnv ::  Trafo m t s (FinalEnv t s -> FinalEnv t s) ()
+updateFinalEnv = Trafo $ \m -> (TrafoE m (\f' t e f -> ((), t, e, f' . f)))
+
+
 -- | The function 'extEnv' returns a 'TrafoE' that extends the current environment.
 extEnv :: m (e,a) -> TrafoE m t s e (t a s) (Ref a s)
-extEnv m = TrafoE m $ \ta  (T tr) env  ->  (tr Zero,  T (tr P.. Suc),  Ext env ta )
+extEnv m = TrafoE m $ \ta  (T tr) env  f ->  (tr Zero,  T (tr P.. Suc),  Ext env ta, f )
 
 -- | The function 'castSRef'  returns a 'TrafoE' that casts the reference 
 --   passed as parameter (in the constructed environment) to one in the final environment.
 castSRef :: m e -> Ref a e -> TrafoE m t s e x (Ref a s)
-castSRef m r = TrafoE m $ (\   _ (T t) decls  ->  (t r, T t, decls))
+castSRef m r = TrafoE m $ (\   _ (T t) decls f ->  (t r, T t, decls, f))
 
 -- | The function 'updateSRef' returns a 'TrafoE' that updates the value pointed
 --   by the reference passed as parameter into the current environment.
 updateSRef :: m e -> Ref a e -> (i -> t a s -> t a s) -> TrafoE m t s e i (Ref a s)
-updateSRef m r f = TrafoE m $ \i (T t) decls -> (t r, T t, updateEnv (f i) r decls)
+updateSRef m r f = TrafoE m $ \i (T t) decls fs -> (t r, T t, updateEnv (f i) r decls, fs)
 
 
 instance Functor (TrafoE m t s e a) where
- fmap f (TrafoE m step) = TrafoE m $ \i t e -> case step i t e of
-                                               (i',t',e') -> (f i',t',e')
+ fmap f (TrafoE m step) = TrafoE m $ \i t e fs -> case step i t e fs of
+                                                  (i',t',e',fs') -> (f i',t',e',fs')
 
 -- | The type 'Result' is the type of the result of \"running\" a 'Trafo'. 
 --   Because @s@ could be anything we have to hide it using existential quantification.
@@ -218,11 +241,11 @@
 runTrafo trafo m a = case trafo of
   Trafo trf -> case trf m of
                    TrafoE m2 f -> 
-                     case  f a (T unsafeCoerce) Empty of
-                       (rb, _, env2) -> 
+                     case  f a (T unsafeCoerce) Empty P.id of  -- the function could also be passed as argument
+                       (rb, _, env2, fenvs) -> 
                          Result  (unsafeCoerce m2)  
                                  rb 
-                                 (unsafeCoerce env2) 
+                                 (fenvs $ unsafeCoerce env2) 
 
 #if __GLASGOW_HASKELL__ >= 609
 
@@ -235,15 +258,15 @@
                                        TrafoE m3 f2 ->
                                         TrafoE 
                                         m3 
-                                        (\a  tt env1 ->
-                                             let  (b,tt1, env2) = f1 a tt2 env1
-                                                  (c,tt2, env3) = f2 b tt env2
-                                             in   (c,tt1, env3)                                                                    
+                                        (\a  tt env1 fs ->
+                                             let  (b,tt1, env2, fs')   = f1 a tt2 env1 fs
+                                                  (c,tt2, env3, fs'')  = f2 b tt env2 fs'
+                                             in   (c,tt1, env3, fs'')                                                                    
                                         )
   )
 
  -- |id :: Trafo m t s a a|
- id =  Trafo  (\m -> TrafoE m (\a t e -> (a, t, e)) )
+ id =  Trafo  (\m -> TrafoE m (\a t e f -> (a, t, e, f)) )
 
 #endif
 
@@ -251,7 +274,7 @@
 instance Arrow (Trafo m t s) where
 
  -- |arr :: (a  -> b) -> Trafo m t s a b|
- arr f =  Trafo  (\m -> TrafoE m (\a t e -> (f a, t, e)) )
+ arr f =  Trafo  (\m -> TrafoE m (\a t e fs -> (f a, t, e, fs)) )
 
 #if __GLASGOW_HASKELL__ < 609 
 
@@ -262,10 +285,10 @@
                                        TrafoE m3 f2 ->
                                         TrafoE 
                                         m3 
-                                        (\a  tt env1 ->
-                                             let  (b,tt1, env2) = f1 a tt2 env1
-                                                  (c,tt2, env3) = f2 b tt env2
-                                             in   (c,tt1, env3)                                                                    
+                                        (\a  tt env1 fs ->
+                                             let  (b,tt1, env2, fs')   = f1 a tt2 env1 fs
+                                                  (c,tt2, env3, fs'')  = f2 b tt env2 fs'
+                                             in   (c,tt1, env3, fs'')                                                                    
                                         )
   )
 
@@ -277,9 +300,9 @@
         TrafoE m2 f -> 
            TrafoE  
            m2 
-           (\  ~(a,c) tt env1 -> 
-               let (b,tt1,env2) = f a tt env1
-               in  ((b,c),tt1, env2))) 
+           (\  ~(a,c) tt env1 fs -> 
+               let (b,tt1,env2, fs') = f a tt env1 fs
+               in  ((b,c),tt1, env2, fs'))) 
 
 
 instance ArrowLoop (Trafo m t s) where
@@ -289,9 +312,9 @@
    (\m -> case st m of
            TrafoE m1 f1 ->
             TrafoE  m1
-            (\a t e -> 
-              let ((b, x),t1,e1) = f1 ( (a, x)) t e                                                                            
-              in (b,t1,e1)
+            (\a t e f -> 
+              let ((b, x),t1,e1,f') = f1 (a, x) t e f                                                                            
+              in (b,t1,e1,f')
             ))
 
 -- | The combinator 'sequenceA' sequentially composes a list
@@ -309,6 +332,7 @@
 
 
 
+
 -- | Alternative version of 'Trafo' where the universal quantification 
 --   over |s| is moved inside the quantification over |env2|.
 --   Note that the type variables |a| and |b| are now labelled with |s|, 
@@ -318,10 +342,12 @@
 data  TrafoE2 m t env1 a b = 
   forall env2 .  TrafoE2
                  (m env2)
-                 (forall s .  a s -> T env2 s -> Env t s env1
-                              -> (b s, T env1 s, Env t s env2)
+                 (forall s .  a s -> T env2 s -> Env t s env1 -> UpdFinalEnv t s
+                              -> (b s, T env1 s, Env t s env2, UpdFinalEnv t s)
                  )
 
+newtype UpdFinalEnv t s = Upd (FinalEnv t s -> FinalEnv t s)
+
 -- | The function 'runTrafo2' takes as arguments the 'Trafo2' we want to run, meta-information 
 --   for the empty environment, and an input value. 
 --   The result of 'runTrafo2' (type 'Result') is the final environment (@Env t s s@) together 
@@ -336,9 +362,10 @@
  case trafo of
   Trafo2 trf -> case trf m of
                    TrafoE2 m2 f -> 
-                      let  (rb, _, env2) =  f a (T P.id) Empty 
-                      in   Result m2  rb env2
+                      let  (rb, _, env2, Upd upds) =  f a (T P.id) Empty (Upd P.id)
+                      in   Result m2  rb (upds env2)
 
+
 -- |  The Trafo2 'newSRef2' takes a typed term as input, adds it to the environment 
 --    and yields a reference pointing to this value.
 --    No meta-information on the environment is recorded by 'newSRef2';
@@ -348,12 +375,20 @@
     =  Trafo2  
        (\Unit ->  TrafoE2  
                   Unit
-                  (\ta (T tr) env ->
+                  (\ta (T tr) env upds ->
                       ( tr Zero
                       , T (tr P.. Suc)
                       , Ext env ta
+                      , upds
        )          )   )
 
+
+-- | The function 'updateFinalEnv2' returns a 'Trafo2' that introduces a function
+--   (@(UpdFinalEnv t)@) to update the final environment.
+updateFinalEnv2 ::  Trafo2 m t (UpdFinalEnv t) Unit
+updateFinalEnv2 = Trafo2 $ \m -> (TrafoE2 m (\(Upd u') t e (Upd u) -> (Unit, t, e, (Upd $ u' P.. u))))
+
+
 newtype Pair a b s = P (a s, b s)
 
 class Category2 cat where
@@ -373,7 +408,7 @@
 
 
 instance Category2 (Trafo2 m t) where
-  id2   =  Trafo2  (\m -> TrafoE2 m (\a t e -> (a, t, e)))
+  id2   =  Trafo2  (\m -> TrafoE2 m (\a t e u -> (a, t, e, u)))
 
   (.:.) (Trafo2 sb) (Trafo2 sa) = 
     Trafo2 
@@ -383,9 +418,9 @@
          TrafoE2 m3 f2 -> 
            TrafoE2  
            m3 
-           (\a t3s e1 -> let  (b, t1s, e2) = f1 a t2s e1
-                              (c, t2s, e3) = f2 b t3s e2
-                         in   (c, t1s, e3)
+           (\a t3s e1 u1 -> let  (b, t1s, e2, u2) = f1 a t2s e1 u1
+                                 (c, t2s, e3, u3) = f2 b t3s e2 u2
+                            in   (c, t1s, e3, u3)
            ))
 
 
@@ -395,7 +430,7 @@
  
 instance Arrow2 (Trafo2 m t) where
   arr2 f 
-    =  Trafo2  (\m -> TrafoE2 m (\a t e -> (f a, t, e)) )
+    =  Trafo2  (\m -> TrafoE2 m (\a t e u -> (f a, t, e, u)) )
 
   
   first2 (Trafo2 s) 
@@ -403,9 +438,9 @@
        (\m1 -> case s m1 of
           TrafoE2 m2 f -> 
              TrafoE2  m2
-                    (\(P (a, c)) t2s e1 -> 
-                                      let (b,t12,e2) = f a t2s e1 
-                                      in  (P (b, c),t12,e2)
+                    (\(P (a, c)) t2s e1 u1 -> 
+                                      let (b,t12,e2,u2) = f a t2s e1 u1 
+                                      in  (P (b, c),t12,e2,u2)
                     )              
        ) 
 
@@ -423,9 +458,9 @@
     (\m -> case st m of
             TrafoE2 m1 f1 ->
              TrafoE2  m1
-             (\a t e -> 
-               let (P (b, x),t1,e1) = f1 (P (a, x)) t e                                                                            
-               in (b,t1,e1)
+             (\a t e u -> 
+               let (P (b, x),t1,e1,u1) = f1 (P (a, x)) t e u                                                                            
+               in (b,t1,e1,u1)
              ) 
     )