--- a/nat.agda	Thu Jul 25 14:46:02 2013 +0900
+++ b/nat.agda	Fri Jul 26 06:39:24 2013 +0900
@@ -203,27 +203,36 @@
      join k ( join k h g) f 
   ∎ where open ≈-Reasoning (A) 
 
-KHom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A )  {a b : Obj A} →  {!!} -> {!!} -> Set c₂
-KHom = {!!}
+KHom1 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A )  (a : Obj A) → (b : Obj A)  -> Set (c₂ ⊔ c₁)
+KHom1 = {!!}
+
+record KHom  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( T : Functor A A )  (a : Obj A)  (b : Obj A)
+     : Set (suc (c₂ ⊔ c₁)) where
+   field
+       KMap :  Hom A a ( FObj T b )
 
 Kleisli-join : {!!}
 Kleisli-join = {!!}
 
-Kleisli-id : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( T : Functor A A )  {a : Obj A} → Hom A a (FObj T a)
-Kleisli-id A T = {!!}
+Kleisli-id : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( T : Functor A A ) (η : NTrans A A identityFunctor T) {a : Obj A} → KHom A T a a
+Kleisli-id A T η {a = a} = record { KMap =  TMap η a } 
 
 Lemma10 : {!!}
 Lemma10 = {!!}
 
 open import Relation.Binary.Core
 
+_⋍_ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( T : Functor A A ) 
+    { a : Obj A } { b : Obj A } (f g  : KHom A T a b ) -> Set ?
+_⋍_ = ?
+
 isKleisliCategory : {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 η μ )
                  { k : Kleisli A T η μ m} →
-         IsCategory ( Obj A ) ( KHom A T ) ( Category._≈_ A ) ( Kleisli-join ) (Kleisli-id A T)
+         IsCategory ( Obj A ) ( KHom A T ) ( _⋍_ A T ) ( Kleisli-join ) (Kleisli-id A T η)
 isKleisliCategory A {T} {η} m = record  { isEquivalence =  IsCategory.isEquivalence ( Category.isCategory A )
                     ; identityL =   {!!}
                     ; identityR =   {!!}