--- a/nat.agda	Sat Jul 06 03:30:31 2013 +0900
+++ b/nat.agda	Sat Jul 06 07:27:57 2013 +0900
@@ -33,9 +33,8 @@
   field
     naturality : {a b : Obj D} {f : Hom D a b} 
       → C [ C [ (  FMap G f ) o  ( Trans a ) ]  ≈ C [ (Trans b ) o  (FMap F f)  ] ]
---     how to write uniquness?
 --    uniqness : {d : Obj D} 
---      →  ∃{e : Trans d} -> ∀{a : Trans d}  → C [ e  ≈ a ]
+--      →  C [ Trans d  ≈ Trans d ]
 
 
 record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
@@ -64,9 +63,9 @@
                  ( μ : 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) ] ]
-      unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
-      unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+      assoc  : {a : Obj A} -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
+      unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+      unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η a ))] ≈ Id {_} {_} {_} {A} (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
@@ -88,14 +87,81 @@
     -> A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
 Lemma4 = \a -> IsCategory.identityL ( Category.isCategory a )
 
+Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
+                 { T : Functor A A }
+                 { η : NTrans A A identityFunctor T }
+                 { μ : NTrans A A (T ○ T) T }
+                 { a : Obj A } ->
+                 ( M : Monad A T η μ )
+    ->  A [ A [ Trans μ a o Trans η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+Lemma5 = \m -> IsMonad.unity1 ( isMonad m )
+
+Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
+                 { T : Functor A A }
+                 { η : NTrans A A identityFunctor T }
+                 { μ : NTrans A A (T ○ T) T }
+                 { a : Obj A } ->
+                 ( M : Monad A T η μ )
+    ->  A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
+Lemma6 = \m -> IsMonad.unity2 ( isMonad m )
+
+-- T = M x A
+
+-- open import Data.Product -- renaming (_×_ to _*_)
+
+-- MonoidalMonad : 
+-- MonoidalMonad = record { Obj = M × A 
+--                  ; Hom = _⟶_
+--                  ; Id = IdProd
+--                  ; _o_ = _∘_
+--                  ; _≈_ = _≈_
+--                  ; isCategory = record { isEquivalence = record { refl  = λ {φ} → ≈-refl {φ = φ}
+--                                                                 ; sym   = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
+--                                                                 ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
+--                                                                 }
+--                                        ; identityL = identityL
+--                                        ; identityR = identityR
+--                                        ; o-resp-≈ = o-resp-≈
+--                                        ; associative = associative
+--                                        }
+--                  }
+
+
 -- nat of η
 
 
 -- g ○ f = μ(c) T(g) f
-
 -- h ○ (g ○ f) = (h ○ g) ○ f
 
 -- η(b) ○ f = f
 -- f ○ η(a) = f
 
 
+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
+     infix 9 _*_
+     _*_ : { a b c : Obj A } ->
+                      ( Hom A b ( FObj T c )) -> (  Hom A a ( FObj T b)) -> Hom A a ( FObj T c )
+     g * f = A [ Trans μ ({!!} (Category.cod A g))  o A [ FMap T g  o f ] ]
+
+
+
+-- Kleisli :
+-- Kleisli = record { Hom = 
+--                 ; Hom = _⟶_
+--                  ; Id = IdProd
+--                  ; _o_ = _∘_
+--                  ; _≈_ = _≈_
+--                  ; isCategory = record { isEquivalence = record { refl  = λ {φ} → ≈-refl {φ = φ}
+--                                                                 ; sym   = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
+--                                                                 ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
+--                                                                 }
+--                                        ; identityL = identityL
+--                                        ; identityR = identityR
+--                                        ; o-resp-≈ = o-resp-≈
+--                                        ; associative = associative
+--                                        }
+--                  }