--- a/adj-monad.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/adj-monad.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -32,7 +32,7 @@
      Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○  U} {identityFunctor} ε F)  ) where
          lemma11 :   NTrans A A   ( U ○ ((F  ○  U) ○  F )) ( U ○  (identityFunctor ○ F) ) 
                   →  NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
-         lemma11  n = record { TMap = \a → TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }}
+         lemma11  n = record { TMap = \a → TMap n a; isNTrans = record { commute = IsNTrans.commute ( isNTrans n ) }}
 
 Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                  { U : Functor B A }
@@ -53,7 +53,7 @@
            μ = UεF A B U F ε
            lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) → 
                  B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ] 
-           lemma-assoc1 f =  IsNTrans.naturality ( isNTrans ε )
+           lemma-assoc1 f =  IsNTrans.commute ( isNTrans ε )
            assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
            assoc1 {a} = let open ≈-Reasoning (A) in
              begin