--- a/nat.agda	Sat Jul 06 00:34:08 2013 +0900
+++ b/nat.agda	Sat Jul 06 02:15:24 2013 +0900
@@ -1,33 +1,22 @@
-
-
 module nat  where 
 
-
 -- Monad
 -- Category A
-
 -- A = Category
-
 -- Functor T : A -> A
-
-
-
 --T(a) = t(a)
 --T(f) = tf(f)
 
---T(g f) = T(g) T(f)
-
 open import Category
 open import Level
 open Functor
 
+--T(g f) = T(g) T(f)
+
 Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) ->  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
      -> A [ ( FMap T (A [ g o f ] ))  ≈ (A [ FMap T g o FMap T f ]) ]
 Lemma1 = \t -> IsFunctor.distr ( isFunctor t )
 
-
-
-
 --        F(f)
 --   F(a) ----> F(b)
 --    |          |
@@ -56,29 +45,33 @@
     isNTrans : IsNTrans domain codomain F G Trans
 
 open NTrans
-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  Trans μ a  ]  ≈ A [ Trans μ b  o  FMap F f ] ]
+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 Trans μ a ]  ≈ A [ Trans μ b o  FMap F f ] ]
 Lemma2 = \n -> IsNTrans.naturality ( isNTrans  n  )
 
 open import Category.Cat
 
-record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-                 ( T : Functor A A )
-                 ( η : NTrans A A (identityFunctor) T )
-                 ( μ : NTrans A A T (T ○ T))
-                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-  field
-    unity1 : {a b : Obj A} 
-      → A [ A [ ( Trans μ a ) o ( Trans η a) ] ≈ Id A a ]
-
 -- η :   1_A -> T
 -- μ :   TT -> T
 -- μ(a)η(T(a)) = a
 -- μ(a)T(η(a)) = a
 -- μ(a)(μ(T(a))) = μ(a)T(μ(a))
 
+record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
+                 ( T : Functor A A )
+                 ( η : NTrans A A identityFunctor T )
+                 ( μ : NTrans A A (T ○ T) T)
+                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+   field
+      assoc  : {a : Obj A} -> A [ A [  Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
+--      unity2 : {a : Obj A} -> A [ Trans μ a o (FMap T (Trans η a )) ]
+--      unity1 : {a : Obj A} -> A [ Trans μ a o Trans η ( FObj T a ) ]
 
-
+record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
+       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+  field
+    isMonad : IsMonad A T η μ
 
 
 -- nat of η