--- a/nat.agda	Thu Jul 25 13:56:16 2013 +0900
+++ b/nat.agda	Thu Jul 25 14:46:02 2013 +0900
@@ -203,41 +203,44 @@
      join k ( join k h g) f 
   ∎ where open ≈-Reasoning (A) 
 
--- Kleisli-join : {!!}
--- Kleisli-join = {!!}
+KHom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A )  {a b : Obj A} →  {!!} -> {!!} -> Set c₂
+KHom = {!!}
+
+Kleisli-join : {!!}
+Kleisli-join = {!!}
 
--- Kleisli-id : {!!}
--- Kleisli-id = {!!}
+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 = {!!}
 
--- Lemma10 : {!!}
--- Lemma10 = {!!}
+Lemma10 : {!!}
+Lemma10 = {!!}
 
--- open import Relation.Binary.Core
+open import Relation.Binary.Core
 
--- 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 ) ( Hom A ) ( Category._≈_ A ) ( Kleisli-join ) Kleisli-id
--- isKleisliCategory A {T} {η} m = record  { isEquivalence =  IsCategory.isEquivalence ( Category.isCategory A )
---                     ; identityL =   {!!}
---                     ; identityR =   {!!}
---                     ; o-resp-≈ =    {!!}
---                     ; associative = {!!}
---                     }
---      where
---          KidL : {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 η μ ) → {!!}
---          KidL = {!!}
---          KidR : {!!}
---          KidR = {!!}
---          Ko-resp : {!!}
---          Ko-resp = {!!}
---          Kassoc : {!!}
---          Kassoc = {!!}
+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)
+isKleisliCategory A {T} {η} m = record  { isEquivalence =  IsCategory.isEquivalence ( Category.isCategory A )
+                    ; identityL =   {!!}
+                    ; identityR =   {!!}
+                    ; o-resp-≈ =    {!!}
+                    ; associative = {!!}
+                    }
+     where
+         KidL : {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 η μ ) → {!!}
+         KidL = {!!}
+         KidR : {!!}
+         KidR = {!!}
+         Ko-resp : {!!}
+         Ko-resp = {!!}
+         Kassoc : {!!}
+         Kassoc = {!!}
 
 -- Kleisli :
 -- Kleisli = record { Hom =