Mercurial > hg > Members > kono > Proof > category

changeset 130:5f331dfc000b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove Kleisli record
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 08 Aug 2013 22:05:41 +0900
parents fdf89038556a
children eb7ca6b9d327
files HomReasoning.agda adj-monad.agda cat-utility.agda comparison-functor-conv.agda comparison-functor.agda em-category.agda list-nat.agda monoid-monad.agda nat.agda universal-mapping.agda
diffstat 10 files changed, 111 insertions(+), 130 deletions(-) [+]
line wrap: on
line diff
--- a/HomReasoning.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/HomReasoning.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -21,17 +21,17 @@
                  (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
                  : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
   field
-    naturality : {a b : Obj D} {f : Hom D a b} 
+    commute : {a b : Obj D} {f : Hom D a b} 
       → C [ C [ (  FMap G f ) o  ( TMap a ) ]  ≈ C [ (TMap b ) o  (FMap F f)  ] ]
 
-record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
+record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) 
+     (F G : Functor domain codomain )
        : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
   field
     TMap :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
     isNTrans : IsNTrans domain codomain F G TMap
 
 
-
 module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
   open import Relation.Binary.Core 
 
@@ -113,7 +113,7 @@
          {a b : Obj D} {f : Hom D a b}  {F G : Functor D A }
       →  (η : NTrans D A F G )
       →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
-  nat η  =  IsNTrans.naturality ( isNTrans η  )
+  nat η  =  IsNTrans.commute ( isNTrans η  )
 
   infixr  2 _∎
   infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
--- 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
--- a/cat-utility.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/cat-utility.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -76,18 +76,23 @@
           mu = μ
           field
             isMonad : IsMonad A T η μ
+             -- g ○ f = μ(c) T(g) f
+          join : { a b : Obj A } → { c : Obj A } →
+                              ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
+          join {_} {_} {c} g f = A [ TMap μ c  o A [ FMap T g o f ] ]
+
 
         Functor*Nat :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
             (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○  G) (F ○ H)
         Functor*Nat A {B} C F {G} {H} n = record {
                TMap  = \a -> FMap F (TMap n a)
                ; isNTrans = record {
-                    naturality = naturality
+                    commute = commute
                }
             } where
-                 naturality : {a b : Obj A} {f : Hom A a b} 
+                 commute : {a b : Obj A} {f : Hom A a b} 
                     → C [ C [ (FMap F ( FMap H f )) o  ( FMap F (TMap n a)) ]  ≈ C [ (FMap F (TMap n b )) o  (FMap F (FMap G f))  ] ]
-                 naturality  {a} {b} {f}  = let open ≈-Reasoning (C) in
+                 commute  {a} {b} {f}  = let open ≈-Reasoning (C) in
                     begin  
                        (FMap F ( FMap H f )) o  ( FMap F (TMap n a))
                     ≈⟨ sym (distr F) ⟩
@@ -103,24 +108,12 @@
         Nat*Functor A {B} C {G} {H} n F = record {
                TMap  = \a -> TMap n (FObj F a)
                ; isNTrans = record {
-                    naturality = naturality
+                    commute = commute
                }
             } where
-                 naturality : {a b : Obj A} {f : Hom A a b} 
+                 commute : {a b : Obj A} {f : Hom A a b} 
                     → C [ C [ ( FMap H (FMap F f )) o  ( TMap n (FObj F a)) ]  ≈ C [ (TMap n (FObj F b )) o  (FMap G (FMap F f))  ] ]
-                 naturality  {a} {b} {f}  =  IsNTrans.naturality ( isNTrans n) 
-
-        record Kleisli  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
-                         ( T : Functor A A )
-                         ( η : NTrans A A identityFunctor T )
-                         ( μ : NTrans A A (T ○ T) T )
-                         ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-             monad : Monad A T η μ 
-             monad = M
-             -- g ○ f = μ(c) T(g) f
-             join : { a b : Obj A } → { c : Obj A } →
-                              ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
-             join {_} {_} {c} g f = A [ TMap μ c  o A [ FMap T g o f ] ]
+                 commute  {a} {b} {f}  =  IsNTrans.commute ( isNTrans n) 
 
         -- T ≃  (U_R ○ F_R)
         -- μ = U_R ε F_R
--- a/comparison-functor-conv.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/comparison-functor-conv.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -21,7 +21,6 @@
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
                  { M' : Monad A T η μ }
-                 { K' : Kleisli A T η μ M' } 
       {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) 
       { U_K : Functor B A } { F_K : Functor A B }
       { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
@@ -32,7 +31,7 @@
       ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K} AdjK )
   where
 
-open import nat {c₁} {c₂} {ℓ} {A} { T } { η } { μ } { M' } { K' }
+open import nat {c₁} {c₂} {ℓ} {A} { T } { η } { μ } { M' } 
 open Functor
 open NTrans
 open Category.Cat.[_]_~_
--- a/comparison-functor.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/comparison-functor.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -20,7 +20,6 @@
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
                  { M' : Monad A T η μ }
-                 { K' : Kleisli A T η μ M' } 
       {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) 
       { U_K : Functor B A } { F_K : Functor A B }
       { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
@@ -41,14 +40,10 @@
 -- M =  Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
 M =  Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK
 
-K : Kleisli A (U_K ○ F_K ) η_K μ_K M 
-K = record {}
-
-open import nat {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } { K }
+open import nat {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } 
 
 open Functor
 open NTrans
-open Kleisli
 open KleisliHom
 open Adjunction
 open MResolution
--- a/em-category.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/em-category.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -238,9 +238,9 @@
 
 η^T : NTrans A A identityFunctor ( U^T ○ F^T ) 
 η^T = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
-       naturality1 :  {a b : Obj A} {f : Hom A a b}
+       commute1 :  {a b : Obj A} {f : Hom A a b}
             → A [ A [ ( FMap ( U^T ○ F^T ) f ) o  ( TMap η a ) ]  ≈ A [ (TMap η b ) o  f  ] ]
-       naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+       commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           begin
               ( FMap ( U^T ○ F^T ) f ) o  ( TMap η a )
           ≈⟨ sym (resp refl-hom (Lemma-EM7 f)) ⟩
@@ -249,7 +249,7 @@
               TMap η b o f
           ∎
        isNTrans1 : IsNTrans A A identityFunctor ( U^T ○ F^T ) (\a -> TMap η a)
-       isNTrans1 = record { naturality = naturality1 }
+       isNTrans1 = record { commute = commute1 }
 
 Lemma-EM9 : (a : EMObj) -> A [ A [ (φ a)  o FMap T (φ a) ]  ≈ A [ (φ a)  o (φ (FObj ( F^T ○ U^T ) a)) ] ]
 Lemma-EM9 a = let open ≈-Reasoning (A) in
@@ -266,9 +266,9 @@
 
 ε^T : NTrans Eilenberg-MooreCategory Eilenberg-MooreCategory  ( F^T ○ U^T ) identityFunctor
 ε^T = record { TMap = \a -> emap-ε a; isNTrans = isNTrans1 } where
-       naturality1 : {a b : EMObj } {f : EMHom a b}
+       commute1 : {a b : EMObj } {f : EMHom a b}
             →  (f ∙ ( emap-ε a ) ) ≗ (( emap-ε b ) ∙(  FMap (F^T ○ U^T) f ) )
-       naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+       commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           sym ( begin 
              EMap (( emap-ε b ) ∙ (  FMap (F^T ○ U^T) f ))
           ≈⟨⟩
@@ -279,7 +279,7 @@
              EMap (f ∙ ( emap-ε a ))
           ∎  )
        isNTrans1 : IsNTrans  Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (\a -> emap-ε a )
-       isNTrans1 = record { naturality = \{a} {b} {f} ->  (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) )  (homomorphism f ) }  -- naturity1 {a} {b} {f}
+       isNTrans1 = record { commute = \{a} {b} {f} ->  (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) )  (homomorphism f ) }  -- naturity1 {a} {b} {f}
                                                                                  
 --
 -- μ = U^T ε U^F
@@ -290,9 +290,9 @@
 
 μ^T : NTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T )
 μ^T = record { TMap = emap-μ ; isNTrans = isNTrans1 } where
-        naturality1 : {a b : Obj A} {f : Hom A a b}
+        commute1 : {a b : Obj A} {f : Hom A a b}
              →  A [ A [ (FMap (U^T ○ F^T) f) o  ( emap-μ a) ]  ≈ A [ ( emap-μ b ) o  FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f)  ] ]
-        naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+        commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           sym ( begin 
              ( emap-μ b ) o  FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f) 
           ≈⟨⟩
@@ -305,7 +305,7 @@
              (FMap (U^T ○ F^T) f) o  ( emap-μ a)
           ∎  )
         isNTrans1 : IsNTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) emap-μ
-        isNTrans1 = record { naturality = naturality1 }
+        isNTrans1 = record { commute = commute1 }
 
 Lemma-EM10 : {x : Obj A } -> A [ TMap μ^T x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
 Lemma-EM10 {x} = let open ≈-Reasoning (A) in
--- a/list-nat.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/list-nat.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -3,32 +3,37 @@
 open import Level
 
 
-postulate a : Set
-postulate b : Set
-postulate c : Set
+postulate A : Set
+postulate B : Set
+postulate C : Set
 
+postulate a : A
+postulate b : A
+postulate c : A
+postulate d : B
 
 infixr 40 _::_
-data  List {a} (A : Set a) : Set a where
+data  List  (A : Set ) : Set  where
    [] : List A
    _::_ : A -> List A -> List A
 
 
 infixl 30 _++_
-_++_ : ∀ {a} {A : Set a} -> List A -> List A -> List A
+_++_ :   {A : Set } -> List A -> List A -> List A
 []        ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
 l1 = a :: []
+-- l1' = A :: []
 l2 = a :: b :: a :: c ::  []
 
 l3 = l1 ++ l2
 
-data Node {a} ( A : Set a ) : Set a where
+data Node  ( A : Set  ) : Set  where
    leaf  : A -> Node A
    node  : Node A -> Node A -> Node A
 
-flatten : ∀{n} { A : Set n } -> Node A -> List A
+flatten :  { A : Set } -> Node A -> List A
 flatten ( leaf a )   = a :: []
 flatten ( node a b ) = flatten a ++ flatten b
 
@@ -38,21 +43,21 @@
 
 infixr 20  _==_
 
-data _==_ {n} {A : Set n} :  List A -> List A -> Set n where
+data _==_  {A : Set } :  List A -> List A -> Set  where
       reflection  : {x : List A} -> x == x
 
-cong1 : ∀{a} {A : Set a } {b} { B : Set b } ->
+cong1 :  {A : Set  }  { B : Set  } ->
    ( f : List A -> List B ) -> {x : List A } -> {y : List A} -> x == y -> f x == f y
 cong1 f reflection = reflection
 
-eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) -> x ==  y -> ( a :: x ) == ( a :: y )
+eq-cons :   {A : Set } {x y : List A} ( a : A ) -> x ==  y -> ( a :: x ) == ( a :: y )
 eq-cons a z = cong1 ( \x -> ( a :: x) ) z
 
-trans-list :  ∀{n} {A : Set n} {x y z : List A}  -> x ==  y -> y == z -> x == z
+trans-list :   {A : Set } {x y z : List A}  -> x ==  y -> y == z -> x == z
 trans-list reflection reflection = reflection
 
 
-==-to-≡ :  ∀{n} {A : Set n}  {x y : List A}  -> x ==  y -> x ≡ y
+==-to-≡ :   {A : Set }  {x y : List A}  -> x ==  y -> x ≡ y
 ==-to-≡ reflection = refl
 
 list-id-l : { A : Set } -> { x : List A} ->  [] ++ x == x
@@ -68,7 +73,7 @@
 list-assoc  (x :: xs)  ys zs = eq-cons x ( list-assoc xs ys zs )
 
 
-module ==-Reasoning {n} (A : Set n ) where
+module ==-Reasoning  (A : Set  ) where
 
   infixr  2 _∎
   infixr 2 _==⟨_⟩_ _==⟨⟩_
@@ -76,7 +81,7 @@
 
 
   data _IsRelatedTo_ (x y : List A) :
-                     Set n where
+                     Set  where
     relTo : (x≈y : x  == y  ) → x IsRelatedTo y
 
   begin_ : {x : List A } {y : List A} →
@@ -94,11 +99,11 @@
   _∎ : (x : List A ) → x IsRelatedTo x
   _∎ _ = relTo reflection
 
-lemma11 : ∀{n} (A : Set n) ( x : List A ) -> x == x
+lemma11 :  (A : Set ) ( x : List A ) -> x == x
 lemma11 A x =  let open ==-Reasoning A in
      begin x ∎
       
-++-assoc : ∀{n} (L : Set n) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
+++-assoc :  (L : Set ) ( xs ys zs : List L ) -> (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
 ++-assoc A [] ys zs = let open ==-Reasoning A in
   begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)
    ( [] ++ ys ) ++ zs
@@ -122,35 +127,3 @@
   ∎
 
 
-
---data Bool : Set where
---      true  : Bool
---      false : Bool
-
-
---postulate Obj : Set
-
---postulate Hom : Obj -> Obj -> Set
-
-
---postulate  id : { a : Obj } -> Hom a a
-
-
---infixr 80 _○_
---postulate  _○_ : { a b c  : Obj } -> Hom b c -> Hom a b -> Hom a c
-
--- postulate  axId1 : {a  b : Obj} -> ( f : Hom a b ) -> f == id ○ f
--- postulate  axId2 : {a  b : Obj} -> ( f : Hom a b ) -> f == f ○ id
-
---assoc : { a b c d : Obj } ->
---    (f : Hom c d ) -> (g : Hom b c) -> (h : Hom a b) ->
---    (f ○ g) ○ h == f ○ ( g ○ h)
-
-
---a = Set
-
--- ListObj : {A : Set} -> List A
--- ListObj =  List Set
-
--- ListHom : ListObj -> ListObj -> Set
-
--- a/monoid-monad.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/monoid-monad.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -1,18 +1,18 @@
 open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Category.Monoid
+open import Algebra
 open import Level
---open import Category.HomReasoning                                                                                                               
+module monoid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ }  where
+
+open import Category.HomReasoning                                                                                                               
 open import HomReasoning
 open import cat-utility
 open import Category.Cat
 open import Category.Sets
-open import Algebra
-open import Category.Monoid
 open import Data.Product
 open import Relation.Binary.Core
 open import Relation.Binary
 
-module monooid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ }  where
-
 
 MC :  Category (suc zero) c (suc (ℓ ⊔ c))
 MC = MONOID Mono
@@ -33,5 +33,29 @@
         cong1 refl = refl
 
 
+-- Forgetful Functor
 
+open Functor 
+F : Functor MC Sets
+F  = record {
+        FObj = \a -> { s : Obj Sets } -> s 
+        ; FMap = \f -> ? -- {a : Obj Sets} { g : Hom Sets (FObj F *)  (FObj F ((Mor MC f) *)) } -> g
+        ; isFunctor = record {
+             identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
+             ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
+--             ; ≈-cong = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
+        } 
+    } 
 
+-- Gerator
+
+G : Functor Sets MC
+G  = record {
+        FObj = \a -> * 
+        ; FMap = \f -> { g : Hom MC * * } -> Mor MC 
+        ; isFunctor = record {
+             identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory MC ))
+             ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory MC )))
+             ; ≈-cong = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory MC )))
+        } 
+    } 
--- a/nat.agda	Sat Aug 03 10:12:00 2013 +0900
+++ b/nat.agda	Thu Aug 08 22:05:41 2013 +0900
@@ -24,9 +24,7 @@
                  { T : Functor A A }
                  { η : NTrans A A identityFunctor T }
                  { μ : NTrans A A (T ○ T) T }
-                 { M : Monad A T η μ } 
-                 { K : Kleisli A T η μ M } where
-
+                 { M : Monad A T η μ }  where
 
 --T(g f) = T(g) T(f)
 
@@ -40,7 +38,7 @@
 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} 
       → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b }
       → A [ A [  FMap G f o TMap μ a ]  ≈ A [ TMap μ b o  FMap F f ] ]
-Lemma2 = \n → IsNTrans.naturality ( isNTrans  n  )
+Lemma2 = \n → IsNTrans.commute ( isNTrans  n  )
 
 -- Laws of Monad
 --
@@ -92,19 +90,18 @@
 -- f ○ η(a) = f               -- right id  (Lemma8)
 -- h ○ (g ○ f) = (h ○ g) ○ f  -- assocation law (Lemma9)
 
-open Kleisli
 -- η(b) ○ f = f
 Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) )
-                      → A  [ join K (TMap η b) f  ≈ f ]
+                      → A  [ join M (TMap η b) f  ≈ f ]
 Lemma7 {_} {b} f = 
   let open ≈-Reasoning (A) in 
      begin  
-         join K (TMap η b) f 
+         join M (TMap η b) f 
      ≈⟨ refl-hom ⟩
          A [ TMap μ b  o A [ FMap T ((TMap η b)) o f ] ]  
      ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
         A [ A [ TMap μ b  o  FMap T ((TMap η b)) ] o f ]
-     ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad K )) )  ⟩
+     ≈⟨ car ( IsMonad.unity2 ( isMonad M) )  ⟩
         A [  id (FObj T b)   o f ]
      ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩
         f
@@ -113,17 +110,17 @@
 -- f ○ η(a) = f
 Lemma8 : { a  : Obj A }  { b : Obj A }
                  ( f : Hom A a ( FObj T b) )
-                      → A  [ join K f (TMap η a)  ≈ f ]
+                      → A  [ join M f (TMap η a)  ≈ f ]
 Lemma8 {a} {b} f = 
   begin
-     join K f (TMap η a) 
+     join M f (TMap η a) 
   ≈⟨ refl-hom ⟩
      A [ TMap μ b  o A [  FMap T f o (TMap η a) ] ]  
   ≈⟨ cdr  ( nat η ) ⟩
      A [ TMap μ b  o A [ (TMap η ( FObj T b)) o f ] ] 
   ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
      A [ A [ TMap μ b  o (TMap η ( FObj T b)) ] o f ] 
-  ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad K )) ) ⟩
+  ≈⟨ car ( IsMonad.unity1 ( isMonad M) ) ⟩
      A [ id (FObj T b)  o f ]
   ≈⟨  IsCategory.identityL (Category.isCategory A)  ⟩
      f
@@ -135,12 +132,12 @@
                  ( h : Hom A c ( FObj T d) )
                  ( g : Hom A b ( FObj T c) ) 
                  ( f : Hom A a ( FObj T b) )
-                      → A  [ join K h (join K g f)  ≈ join K ( join K h g) f ]
+                      → A  [ join M h (join M g f)  ≈ join M ( join M h g) f ]
 Lemma9 {a} {b} {c} {d} h g f = 
   begin 
-     join K h (join K g f)  
+     join M h (join M g f)  
    ≈⟨⟩
-     join K h (                  ( TMap μ c o ( FMap T g o f ) ) )
+     join M h (                  ( TMap μ c o ( FMap T g o f ) ) )
    ≈⟨ refl-hom ⟩
      ( TMap μ d  o ( FMap T h  o  ( TMap μ c o ( FMap T g  o f ) ) ) )
    ≈⟨ cdr ( cdr ( assoc )) ⟩
@@ -185,25 +182,25 @@
    ≈⟨ cdr ( car ( sym ( distr T )))   ⟩
      ( TMap μ d  o ( FMap T ( ( ( TMap μ d )   o ( FMap T h  o g ) ) ) o f ) )
    ≈⟨ refl-hom ⟩
-     join K ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
+     join M ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
    ≈⟨ refl-hom ⟩
-     join K ( join K h g) f 
+     join M ( join M h g) f 
   ∎ where open ≈-Reasoning (A) 
 
 --
 --  o-resp in Kleisli Category ( for Functor definitions )
 --
 Lemma10 :  {a b c : Obj A} -> (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → 
-                          A [ f ≈ g ] → A [ h ≈ i ] → A [ (join K h f) ≈ (join K i g) ]
+                          A [ f ≈ g ] → A [ h ≈ i ] → A [ (join M h f) ≈ (join M i g) ]
 Lemma10 {a} {b} {c} f g h i eq-fg eq-hi = let open ≈-Reasoning (A) in
    begin 
-       join K h f
+       join M h f
    ≈⟨⟩
        TMap μ c  o ( FMap T h  o f )
    ≈⟨ cdr ( IsCategory.o-resp-≈ (Category.isCategory A) eq-fg ((IsFunctor.≈-cong (isFunctor T)) eq-hi )) ⟩
        TMap μ c  o ( FMap T i  o g )
    ≈⟨⟩
-       join K i g
+       join M i g
    ∎
 
 --
@@ -228,7 +225,7 @@
 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
 
 _*_ : { a b c : Obj A } → ( KHom b c) → (  KHom a b) → KHom a c 
-_*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) }
+_*_ {a} {b} {c} g f = record { KMap = join M {a} {b} {c} (KMap g) (KMap f) }
 
 isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id 
 isKleisliCategory  = record  { isEquivalence =  isEquivalence 
@@ -384,7 +381,7 @@
           ≈⟨ sym assoc ⟩
              TMap μ c  o ( (FMap T  (TMap η c o g))  o  (TMap η b o f) )
           ≈⟨⟩
-             join K (TMap η c o g)  (TMap η b o f) 
+             join M (TMap η c o g)  (TMap η b o f) 
           ≈⟨⟩
              KMap  ( ffmap g * ffmap f )
           ∎
@@ -424,9 +421,9 @@
 
 nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) 
 nat-η = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
-       naturality1 :  {a b : Obj A} {f : Hom A a b}
+       commute1 :  {a b : Obj A} {f : Hom A a b}
             → A [ A [ (  FMap ( U_T ○ F_T ) f ) o  ( TMap η a ) ]  ≈ A [ (TMap η b ) o  f  ] ]
-       naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+       commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           begin
               ( FMap ( U_T ○ F_T ) f ) o  ( TMap η a )
           ≈⟨ sym (resp refl-hom (Lemma11-1 f)) ⟩
@@ -435,16 +432,16 @@
               TMap η b o f
           ∎ 
        isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (\a -> TMap η a)
-       isNTrans1 = record { naturality = naturality1 } 
+       isNTrans1 = record { commute = commute1 } 
 
 tmap-ε : (a : Obj A) -> KHom (FObj T a) a
 tmap-ε a = record { KMap = id1 A (FObj T a) }
 
 nat-ε : NTrans KleisliCategory KleisliCategory  ( F_T ○ U_T ) identityFunctor
 nat-ε = record { TMap = \a -> tmap-ε a; isNTrans = isNTrans1 } where
-       naturality1 : {a b : Obj A} {f : KHom a b}
+       commute1 : {a b : Obj A} {f : KHom a b}
             →  (f * ( tmap-ε a ) ) ⋍   (( tmap-ε b ) * (  FMap (F_T ○ U_T) f ) )
-       naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+       commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           sym ( begin
               KMap (( tmap-ε b ) * (  FMap (F_T ○ U_T) f ))
           ≈⟨⟩
@@ -475,7 +472,7 @@
               KMap (f * ( tmap-ε a ))
           ∎ )
        isNTrans1 : IsNTrans  KleisliCategory KleisliCategory ( F_T ○ U_T ) identityFunctor (\a -> tmap-ε a )
-       isNTrans1 = record { naturality = naturality1 } 
+       isNTrans1 = record { commute = commute1 } 
 
 --
 -- μ = U_T ε U_F
@@ -485,9 +482,9 @@
 
 nat-μ : NTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T )
 nat-μ = record { TMap = tmap-μ ; isNTrans = isNTrans1 } where
-        naturality1 : {a b : Obj A} {f : Hom A a b}
+        commute1 : {a b : Obj A} {f : Hom A a b}
              →  A [ A [ (FMap (U_T ○ F_T) f) o  ( tmap-μ a) ]  ≈ A [ ( tmap-μ b ) o  FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f)  ] ]
-        naturality1 {a} {b} {f} =  let open ≈-Reasoning (A) in
+        commute1 {a} {b} {f} =  let open ≈-Reasoning (A) in
           sym ( begin
              ( tmap-μ b ) o  FMap (U_T ○ F_T) ( FMap (U_T ○ F_T) f)  
           ≈⟨⟩
@@ -502,7 +499,7 @@
              (FMap (U_T ○ F_T) f) o  ( tmap-μ a) 
           ∎ )
         isNTrans1 : IsNTrans A A (( U_T ○ F_T ) ○ ( U_T ○ F_T )) ( U_T ○ F_T ) tmap-μ
-        isNTrans1 = record { naturality = naturality1 } 
+        isNTrans1 = record { commute = commute1 } 
 
 Lemma12 : {x : Obj A } -> A [ TMap nat-μ x ≈ FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ]
 Lemma12 {x} = let open ≈-Reasoning (A) in
--- 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 }
 
 ------
 --