# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1374970244 -32400
# Node ID 419923b149caf8e1ef323b15a5ccc3f89a13c8d1
# Parent  4690953794c49250b062620abb21ded7468f1dfc
on going

diff -r 4690953794c4 -r 419923b149ca cat-utility.agda
--- a/cat-utility.agda	Sun Jul 28 08:04:01 2013 +0900
+++ b/cat-utility.agda	Sun Jul 28 09:10:44 2013 +0900
@@ -138,9 +138,14 @@
               { μR : NTrans A A ( (UR ○ FR)  ○ ( UR ○ FR )) ( UR ○ FR  ) }
               ( Adj : Adjunction A B UR FR ηR εR  )
                         : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
+                   -- MObj : (a : Obj A) -> Obj A
+                   -- MObj a = FObj ( UR ○ FR ) a
+                   -- MMap : {a b c d : Obj A} -> (f : Hom A a b) -> Hom A (FObj T a) (FObj T b)
+                   -- MMap f = FMap ( UR ○ FR ) f
                    field
                       T=UF  :  T ≃  (UR ○ FR) 
                       μ=UεF : {x : Obj A } -> A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ]
                       -- ηR=η  : {x : Obj A } -> A [ TMap ηR x  ≈  TMap η x ]
                       -- μR=μ  : {x : Obj A } -> A [ TMap μR x  ≈  TMap μ x ]
 
+
diff -r 4690953794c4 -r 419923b149ca nat.agda
--- a/nat.agda	Sun Jul 28 08:04:01 2013 +0900
+++ b/nat.agda	Sun Jul 28 09:10:44 2013 +0900
@@ -216,13 +216,13 @@
    field
        KMap :  Hom A a ( FObj T b )
 
-KHom  = \(a b : Obj A) -> KleisliHom { c₁} {c₂} {ℓ} {A} {T} a b
+open KleisliHom 
+KHom  = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b
 
 K-id :  {a : Obj A} → KHom a a
 K-id {a = a} = record { KMap =  TMap η a } 
 
 open import Relation.Binary.Core
-open KleisliHom 
 
 _⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ 
 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
@@ -555,17 +555,22 @@
       { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } 
       ( K :  Monad A (U_K ○ F_K) η_K μ_K )
       ( AdjK : Adjunction A B U_K F_K η_K ε_K )
-      (ResK : MResolution A B T M U_K F_K AdjK )
+      ( RK : MResolution A B T M U_K F_K AdjK )
   where
 
+        KtoT : {!!}
+        KtoT = {!!}
         RHom  = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b
-        kfmap : {a b : Obj A} (f : RHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
-        kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (KMap f) ]
+        RMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) 
+        RMap f = KtoT (RK T=UF) f
+
+        kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
+        kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (RMap f) ]
 
         K_T : Functor KleisliCategory B 
         K_T = record {
                   FObj = FObj F_K
-                ; FMap = {!!} -- kfmap
+                ; FMap = kfmap
                 ; isFunctor = record
                 {      ≈-cong   = {!!} -- ≈-cong
                      ; identity = {!!} -- identity