--- a/HomReasoning.agda	Sun Aug 11 16:56:17 2013 +0900
+++ b/HomReasoning.agda	Tue Aug 13 10:57:41 2013 +0900
@@ -73,6 +73,7 @@
   sym :  {a b : Obj A } { f g : Hom A a b } →  f ≈ g  →  g ≈ f
   sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
 
+  sym-hom = sym
 -- How to prove this?
   ≡-≈ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≡ y ) → x ≈ y
   ≡-≈  refl = refl-hom

--- a/monoid-monad.agda	Sun Aug 11 16:56:17 2013 +0900
+++ b/monoid-monad.agda	Tue Aug 13 10:57:41 2013 +0900
@@ -13,22 +13,31 @@
 --    a -> m x a
 --    m x a -> m' x (m x a)
 
+open Monoid
+Lemma-m01 : ( f g :  Carrier M ) ->  Carrier M
+Lemma-m01 f g = _∙_  M f  g
+
 data T1  (M :  Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( ( c₁ ⊔ c₂ ⊔ ℓ) ) where
-   T1a :  Obj A -> T1 M A
-   T1t :  Obj A -> T1 M A -> T1 M A
+   T1a :  Carrier M -> Obj A -> T1 M A
+   T1t :  Carrier M -> T1 M A -> T1 M A 
 
 T1Obj : (a : T1 M A )  -> Obj A
-T1Obj (T1a a1 )  = a1
-T1Obj (T1t a1 t1 )  = a1
+T1Obj (T1a _ a1 )  = a1
+T1Obj (T1t _ t1 )  = T1Obj t1
+
+T1M : (a : T1 M A )  -> Carrier M
+T1M (T1a m _)  = m
+T1M (T1t m _)  = m
+
 
 record T1Hom  (a : T1 M A ) (b : T1 M A) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
    field
        T1Map  : Hom A  (T1Obj a) (T1Obj 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 ] } 
-infixr 9 _∙_ 
+_∘_ :  { 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 ] } 
+infixr 9 _∘_ 
 
 
 T1-id :  {a : T1 M A} → T1Hom a a
@@ -40,8 +49,8 @@
 _⋍_ {a} {b} f g = A [ T1Map f ≈ T1Map g ]
 infix 4 _⋍_ 
 
-isT1Category : IsCategory ( T1 M A ) T1Hom _⋍_ _∙_ T1-id 
-isT1Category  = record  { isEquivalence =  isEquivalence 
+isT1Category : IsCategory ( T1 M A ) T1Hom _⋍_ _∘_ T1-id 
+isT1Category  = record  { isEquivalence =  isEquivalence1
                     ; identityL =   IsCategory.identityL (Category.isCategory A)
                     ; identityR =   IsCategory.identityR (Category.isCategory A)
                     ; o-resp-≈ =    IsCategory.o-resp-≈ ( Category.isCategory A )
@@ -49,11 +58,11 @@
                     }
      where
          open ≈-Reasoning (A) 
-         isEquivalence :  { a b : T1 M A } ->
+         isEquivalence1 :  { a b : T1 M A } ->
                IsEquivalence {_} {_} {T1Hom a b} _⋍_
-         isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
+         isEquivalence1 {C} {D} =      -- this is the same function as A's equivalence but has different types
            record { refl  = refl-hom
-             ; sym   = sym
+             ; sym   = sym-hom
              ; trans = trans-hom
              } 
 
@@ -61,18 +70,25 @@
 T1Category =
   record { Obj = T1 M A
          ; Hom = T1Hom
-         ; _o_ = _∙_
+         ; _o_ = _∘_
          ; _≈_ = _⋍_
          ; Id  = T1-id
          ; isCategory = isT1Category
          }
 
-tobj : ( a : T1 M A ) -> T1 M A
-tobj (T1a a)  =  T1a a
-tobj (T1t a t)  =  T1t a t
+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 ) 
 
-tfmap : {a b : T1 M A } ( f : T1Hom a b ) -> T1Hom (tobj a) (tobj b)
-tfmap f = ? -- record { T1Map = T1Map f }
+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) }
 
 T : Functor T1Category T1Category
 T = record {
@@ -80,14 +96,14 @@
         ; FMap = tfmap
         ; isFunctor = record
         { ≈-cong   = ≈-cong
-             ; identity = identity
+             ; identity = identity1
              ; distr    = distr1
         }
     } where
         ≈-cong   : {a b : T1 M A} {f g : T1Hom a b} → f ⋍ g → tfmap f ⋍ tfmap g
-        ≈-cong   = ?
-        identity : {a : T1 M A} →  ((tfmap (T1-id {a} )) ⋍ (T1-id { tobj a })) 
-        identity = ?
+        ≈-cong   = {!!}
+        identity1 : {a : T1 M A} →  ((tfmap (T1-id {a} )) ⋍ (T1-id { tobj a })) 
+        identity1 = {!!}
         distr1    :  {a b c : T1 M A} {f : T1Hom a b} {g : T1Hom b c} → 
-                 ( tfmap ( g ∙ f) ⋍  ( tfmap g ∙ tfmap f ) )
-        distr1    = ?
+                 ( tfmap ( g ∘ f) ⋍  ( tfmap g ∘ tfmap f ) )
+        distr1    = {!!}