--- a/free-monoid.agda	Fri Apr 18 16:58:54 2014 +0900
+++ b/free-monoid.agda	Fri Apr 18 20:19:32 2014 +0900
@@ -289,7 +289,32 @@
 --   fm-ε b = Φ
 fm-ε :  NTrans B B ( ( FunctorF A B FreeMonoidUniveralMapping) ○ U) identityFunctor
 fm-ε =  nat-ε A B {U} {Generator} {eta} FreeMonoidUniveralMapping 
---  TMap fm-ε
+--   TMap = λ a  →  solution (FObj U a) a (λ x → x ) ;
+--   isNTrans = record {
+--        commute =  commute1 
+--     }
+--   } where
+--     commute1 :  {a b : Obj B} {f : Hom B a b} → let open ≈-Reasoning B  renaming (_o_ to _*_ ) in 
+--                ( FMap (identityFunctor {_} {_} {_} {B}) f * solution (FObj U a) a (λ x → x) ) ≈
+--                (  solution (FObj U b) b (λ x → x) * FMap (FunctorF A B FreeMonoidUniveralMapping ○ U) f )
+--     commute1 {a} {b} {f} = let open ≡-Reasoning in begin
+--              morph ((B ≈-Reasoning.o FMap identityFunctor f) (solution (FObj U a) a (λ x → x)))
+--         ≡⟨ {!!}  ⟩
+--             morph ((B ≈-Reasoning.o solution (FObj U b) b (λ x → x)) (FMap (FunctorF A B FreeMonoidUniveralMapping ○ U) f))
+--         ∎
+
+
+fm-η :  NTrans A A identityFunctor ( U ○ ( FunctorF A B FreeMonoidUniveralMapping) ) 
+fm-η =  record { 
+   TMap = λ a →  λ (x : a) → x :: [] ;
+   isNTrans =  record {
+       commute = commute1
+     }
+  } where
+     commute1 :  {a b : Obj A} {f : Hom A a b} → let open ≈-Reasoning A  renaming (_o_ to _*_ ) in 
+           (( FMap (U ○ FunctorF A B FreeMonoidUniveralMapping) f ) * (λ x → x :: []) ) ≈ ( (λ x → x :: []) * (λ z → FMap (identityFunctor {_} {_} {_} {A}) f z ) )
+     commute1 {a} {b} {f} =  refl   --    λ (x : a ) → f x :: []
+        
 
 open Adjunction