--- a/universal-mapping.agda	Tue Jul 23 03:39:56 2013 +0900
+++ b/universal-mapping.agda	Tue Jul 23 04:10:42 2013 +0900
@@ -208,3 +208,22 @@
              ; distr    = lemma-distr
              }
 
+--
+-- naturality of η
+--
+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  A A identityFunctor ( U ○  FunctorF A B U F η um )
+nat-η A B U F η um = record {
+             TMap = η ; isNTrans = myIsNTrans
+       } where
+    F' : Functor A B
+    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 )
+    myIsNTrans : IsNTrans A A identityFunctor ( U ○  F' ) η
+    myIsNTrans = record { naturality = naturality }