--- a/universal-mapping.agda	Tue Jul 23 04:10:42 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 10:13:09 2013 +0900
@@ -216,7 +216,7 @@
                  ( F : Obj A -> Obj B )
                  ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) ->
        (um : UniversalMapping A B U F η )  -> 
-           NTrans  A A identityFunctor ( U ○  FunctorF A B U F η um )
+           NTrans  A A identityFunctor ( U ○ FunctorF A B U F η um )
 nat-η A B U F η um = record {
              TMap = η ; isNTrans = myIsNTrans
        } where
@@ -224,6 +224,39 @@
     F' = FunctorF A B U F η um
     naturality :  {a b : Obj A} {f : Hom A a b}
       → A [ A [ (FMap U (FMap F' f))  o  ( η a ) ]  ≈ A [ (η b ) o f ] ]
-    naturality {a} {b} =  (IsUniversalMapping.universalMapping ( isUniversalMapping um )) a ( F b )
+    naturality {a} {b} {f} =   let open ≈-Reasoning (A) in
+       begin
+            (FMap U (FMap F' f))  o  ( η a ) 
+       ≈⟨⟩
+            (FMap U ((_* um)  (A [  η b  o f ])))   o  ( η a ) 
+       ≈⟨ (IsUniversalMapping.universalMapping ( isUniversalMapping um )) a ( F b )  ⟩
+            (η b ) o f 
+       ∎
     myIsNTrans : IsNTrans A A identityFunctor ( U ○  F' ) η
     myIsNTrans = record { naturality = naturality }
+
+nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
+                 ( U : Functor B A )
+                 ( F : Obj A -> Obj B )
+                 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) ) ->
+       (um : UniversalMapping A B U F η )  -> 
+           NTrans B B ( FunctorF A B U F η um ○ U) identityFunctor 
+nat-ε A B U F η um = record {
+             TMap = ε ; isNTrans = myIsNTrans
+       } where
+    F' : Functor A B
+    F' = FunctorF A B U F η um
+    ε : ( b : Obj B ) -> Hom B ( FObj F' ( FObj U b) ) b
+    ε b = (_* um) ( id1 A (FObj U b))
+    naturality : {a b : Obj B} {f : Hom B a b }
+      →  B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ]
+    naturality {a} {b} {f} = let open ≈-Reasoning (B) in
+       sym ( begin
+          ε b o (FMap F' (FMap U f))
+       ≈⟨⟩
+          ε b o (FMap F' (FMap U f))
+       ≈⟨ {!!} ⟩
+          f o  (ε a)
+       ∎ )
+    myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor　ε
+    myIsNTrans = record { naturality = naturality }