--- a/nat.agda	Fri Jul 26 16:18:32 2013 +0900
+++ b/nat.agda	Fri Jul 26 19:52:19 2013 +0900
@@ -253,4 +253,83 @@
                           (f * (g * h)) ⋍ ((f * g) * h)
          Kassoc {_} {_} {_} {_} {f} {g} {h} =  Lemma9 (KMap f) (KMap g) (KMap h) 
 
+KleisliCategory : Category c₁ (suc (c₂ ⊔ c₁)) ℓ
+KleisliCategory =
+  record { Obj = Obj A
+         ; Hom = KHom
+         ; _o_ = _*_
+         ; _≈_ = _⋍_
+         ; Id  = K-id
+         ; isCategory = isKleisliCategory
+         }
 
+U_T : Functor KleisliCategory A
+U_T = record {
+        FObj = FObj T
+          ; FMap = ufmap
+        ; isFunctor = record
+        {      ≈-cong   = ≈-cong
+             ; identity = identity
+             ; distr    = distr
+        }
+     } where
+        ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b)
+        ufmap {a} {b} f =  A [ TMap μ (b)  o FMap T (KMap f) ]
+        identity : {a : Obj A} →  A [ ufmap (K-id {a}) ≈ id1 A (FObj T a) ]
+        identity {a} = let open ≈-Reasoning (A) in
+          begin
+              TMap μ (a)  o FMap T (TMap η a)
+          ≈⟨ IsMonad.unity2 (isMonad M) ⟩
+             id1 A (FObj T a)
+          ∎
+        ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ]
+        ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
+          begin
+             TMap μ (b)  o FMap T (KMap f)
+          ≈⟨ cdr (fcong T f≈g) ⟩
+             TMap μ (b)  o FMap T (KMap g)
+          ∎
+        distr :  {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )]
+        distr {_} {_} {c} {f} {g} = let open ≈-Reasoning (A) in
+          begin
+             ufmap (g * f)
+--          ≈⟨⟩
+--             TMap μ (FObj T c)  o FMap T ( (TMap μ (c) o FMap T (KMap g))  o (KMap f))
+          ≈⟨ {!!} ⟩
+             ufmap g o ufmap f
+          ∎
+
+
+ffmap :  {a b : Obj A} (f : Hom A a b) -> KHom a b
+ffmap f = record { KMap = A [ TMap η (Category.cod A f) o f ] }
+
+F_T : Functor A KleisliCategory
+F_T = record {
+        FObj = \a -> a
+        ; FMap = ffmap
+        ; isFunctor = record
+        { ≈-cong   = ≈-cong
+             ; identity = identity
+             ; distr    = distr
+        }
+     } where
+        identity : {a : Obj A} →  A [ A [ TMap η a o id1 A a ] ≈ TMap η a  ]
+        identity {a} = IsCategory.identityR ( Category.isCategory A)
+        lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b  ≈  TMap η b ]
+        lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
+        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η (Category.cod A f) o f ] ≈ A [ TMap η (Category.cod A g) o g ] ]
+        ≈-cong f≈g =  (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1  f≈g )
+        distr :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → 
+                 ( ffmap (A [ g o f ]) ⋍  ( ffmap g * ffmap f ) )
+        distr {_} {_} {_} {f} {g} =  let open ≈-Reasoning (A) in
+          begin
+             KMap (ffmap (A [ g o f ]))
+          ≈⟨ {!!} ⟩
+             KMap  ( ffmap g * ffmap f )
+          ∎
+
+
+
+
+
+