--- a/universal-mapping.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/universal-mapping.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -221,9 +221,9 @@
        } where
     F' : Functor A B
     F' = FunctorF A B um
-    naturality :  {a b : Obj A} {f : Hom A a b}
+    commute :  {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} {f} =   let open ≈-Reasoning (A) in
+    commute {a} {b} {f} =   let open ≈-Reasoning (A) in
        begin
             (FMap U (FMap F' f))  o  ( η a ) 
        ≈⟨⟩
@@ -232,7 +232,7 @@
             (η b ) o f 
        ∎
     myIsNTrans : IsNTrans A A identityFunctor ( U ○  F' ) η
-    myIsNTrans = record { naturality = naturality }
+    myIsNTrans = record { commute = commute }
 
 nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                  { U : Functor B A }
@@ -280,9 +280,9 @@
        ≈⟨ cdr ( IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
           FMap U f o id (FObj U a )
        ∎
-    naturality : {a b : Obj B} {f : Hom B a b }
+    commute : {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
+    commute {a} {b} {f} = let open ≈-Reasoning (B) in
        sym ( begin
           ε b o (FMap F' (FMap U f))
        ≈⟨⟩
@@ -297,7 +297,7 @@
           f o  (ε a)
        ∎ )
     myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor　ε
-    myIsNTrans = record { naturality = naturality }
+    myIsNTrans = record { commute = commute }
 
 ------
 --