--- a/nat.agda	Fri Jul 26 06:39:24 2013 +0900
+++ b/nat.agda	Fri Jul 26 11:42:57 2013 +0900
@@ -211,20 +211,25 @@
    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 ) (η : 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 = {!!}
+K-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
+K-id {_} {_} {_} {A} {T} {η} {a = a} = record { KMap =  TMap η a } 
 
 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 ?
-_⋍_ = ?
+_⋍_ :  ∀{c₁ c₂ ℓ} {A : Category c₁ c₂ ℓ} { T : Functor A A }
+    { a : Obj A } { b : Obj A } (f g  : KHom A T a b ) -> Set (suc ((c₂ ⊔ c₁) ⊔ ℓ))
+_⋍_ = {!!}
+
+
+_*_ :  { 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 } →
+       { 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 )
+_*_ {_} {_} {_} {_} {_} {_} {_} {_} {K} {a} {b} {c} g f = join K {a} {b} {c} g f
 
 isKleisliCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
                  { T : Functor A A }
@@ -232,23 +237,44 @@
                  { μ : NTrans A A (T ○ T) T }
                  ( m : Monad A T η μ )
                  { k : Kleisli A T η μ m} →
-         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 =   {!!}
-                    ; o-resp-≈ =    {!!}
-                    ; associative = {!!}
+         IsCategory ( Obj A ) ( KHom A T ) _⋍_ _*_ K-id 
+isKleisliCategory A {T} {η} m = record  { isEquivalence =  isEquivalence A T
+                    ; identityL =   KidL
+                    ; identityR =   KidR
+                    ; o-resp-≈ =    Ko-resp
+                    ; associative = Kassoc
                     }
      where
-         KidL : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) { T : Functor A A }
+         isEquivalence : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → ( T : Functor A A ) -> { a b : Obj A } ->
+               IsEquivalence {_} {_} {KHom A T a b} _⋍_
+         isEquivalence A T {C} {D} =
+           record { refl  = λ {F} → ⋍-refl {F}
+             ; sym   = λ {F} {G} → ⋍-sym {F} {G}
+             ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H}
+             } where
+                  ⋍-refl : {F : KHom A T C D} → F ⋍ F
+                  ⋍-refl = {!!}
+                  ⋍-sym : {F G : KHom A T C D} → F ⋍ G → G ⋍ F
+                  ⋍-sym = {!!}
+                  ⋍-trans : {F G H : KHom A T C D} → F ⋍ G → G ⋍ H → F ⋍ H
+                  ⋍-trans = {!!}
+         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 η μ ) → {!!}
+                 { μ : NTrans A A (T ○ T) T } { m : Monad A T η μ } → {C D : Obj A} -> {f : KHom A T C D} → (K-id * f) ⋍ f
          KidL = {!!}
-         KidR : {!!}
+         KidR : {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 η μ } → {C D : Obj A} -> {f : KHom A T C D} → (f * K-id) ⋍ f
          KidR = {!!}
-         Ko-resp : {!!}
+         Ko-resp : {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 η μ } → {a b c : Obj A} -> {f g : KHom A T a b } → {h i : KHom A T b c } → 
+                          f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
          Ko-resp = {!!}
-         Kassoc : {!!}
+         Kassoc :  {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 η μ } → {a b c : Obj A} -> {f g : KHom A T a b } → {h i : KHom A T b c } →
+                          (f * (g * h)) ⋍ ((f * g) * h)
          Kassoc = {!!}
 
 -- Kleisli :