--- a/nat.agda	Sat Jul 06 07:27:57 2013 +0900
+++ b/nat.agda	Sat Jul 06 08:50:32 2013 +0900
@@ -137,15 +137,27 @@
 -- f ○ η(a) = f
 
 
-record Kleisli  { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
+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
+     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 [ Trans μ c  o A [ FMap T g  o f ] ]
+
+open Kleisli
+Lemma7 : {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 ] ]
+                 { a b : Obj A } 
+                 { f : Hom A a ( FObj T b) } 
+                 { M : Monad A T η μ } 
+                 ( K : Kleisli A T η μ M) 
+                      -> A  [ join ? ? ?  ≈ f ]
+Lemma7 = \m -> {!!}
+