--- a/monoid-monad.agda	Tue Aug 13 10:57:41 2013 +0900
+++ b/monoid-monad.agda	Tue Aug 13 11:42:09 2013 +0900
@@ -29,19 +29,27 @@
 T1M (T1a m _)  = m
 T1M (T1t m _)  = m
 
+tobj : ( a : T1 M A ) -> {m' : Carrier M } -> T1 M A
+tobj (T1a m a)  {m'}  =  T1t m' ( T1a m a ) 
+tobj (T1t m t)  {m'}  =  T1t m' ( T1t m t ) 
 
 record T1Hom  (a : T1 M A ) (b : T1 M A) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
    field
        T1Map  : Hom A  (T1Obj a) (T1Obj b )
+       P   : Hom A (T1Obj (tobj a {T1M a}) ) (T1Obj a)
+       Q   : Hom A (T1Obj b ) (T1Obj (tobj b {T1M b}) ) 
 
 open T1Hom
 _∘_ :  { a b c : T1 M A } -> T1Hom b c -> T1Hom a b -> T1Hom  a c
-_∘_  g f  =  record { T1Map = A [ T1Map g  o T1Map f ] } 
+_∘_  g f  =  record { T1Map = A [ T1Map g  o T1Map f ] ;
+                      P     = P f;
+                      Q     = Q g
+    } 
 infixr 9 _∘_ 
 
 
-T1-id :  {a : T1 M A} → T1Hom a a
-T1-id {a = a} = record { T1Map =  id1 A (T1Obj a) } 
+T1-id :  {a : T1 M A} → {p : Hom A (T1Obj (tobj a {T1M a}) ) (T1Obj a)} -> {q : Hom A (T1Obj a ) (T1Obj (tobj a {T1M a}) )} -> T1Hom a a
+T1-id {a = a} {p} {q} = record { T1Map =  id1 A (T1Obj a) ; P = p; Q = q } 
 
 open import Relation.Binary.Core
 
@@ -76,19 +84,14 @@
          ; isCategory = isT1Category
          }
 
-tobj : ( a : T1 M A ) -> {m' : Carrier M } -> T1 M A
-tobj (T1a m a)  {m'}  =  T1t m' ( T1a m a ) 
-tobj (T1t m t)  {m'}  =  T1t m' ( T1t m t ) 
-
-tfmap1 : (a b : T1 M A ) (m m' : Carrier M ) ( f : Hom A  (T1Obj a) (T1Obj b) ) -> Hom A (T1Obj (tobj a)) (T1Obj (tobj b))
-tfmap1 (T1a m a) b _ m' f = ?
-tfmap1 (T1t m t) b _ m' f = ?
-
 --  T(f) (m,a)  = (m, f(a) )
 --  T(f) = \(m,a)  -> (m, f(a) )
 --  fmap f = T1 m a -> T1 m (f a)
-tfmap : {a b : T1 M A } {m m' : Carrier M} ( f : T1Hom a b ) -> T1Hom (tobj a {m} ) (tobj b {m'} )
-tfmap {a} {b} {m} {m'} f =  record { T1Map = tfmap1 a b m m' (T1Map f) }
+tfmap : {a b : T1 M A } ( f : T1Hom a b ) -> T1Hom (tobj a {T1M a} ) (tobj b {T1M b} )
+tfmap {a} {b} f =  record { T1Map = A [ Q f  o  A [ (T1Map f)  o P f ] ]  ;
+                            P = ? ;
+                            Q = ? 
+   }
 
 T : Functor T1Category T1Category
 T = record {