--- a/monoid-monad.agda	Tue Aug 13 11:42:09 2013 +0900
+++ b/monoid-monad.agda	Tue Aug 13 11:48:45 2013 +0900
@@ -2,111 +2,35 @@
 open import Category.Monoid
 open import Algebra
 open import Level
-module monoid-monad {c₁ c₂ ℓ : Level} { M : Monoid c₁ ℓ} {A : Category c₁ c₂ ℓ }  where
+module monoid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ }  where
 
+open import Category.HomReasoning                                                                                                               
 open import HomReasoning
 open import cat-utility
 open import Category.Cat
 open import Category.Sets
-
--- T : A -> (M x A)
---    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 :  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 _ t1 )  = T1Obj t1
-
-T1M : (a : T1 M A )  -> Carrier M
-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 ] ;
-                      P     = P f;
-                      Q     = Q g
-    } 
-infixr 9 _∘_ 
+open import Data.Product
+open import Relation.Binary.Core
+open import Relation.Binary
 
 
-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
-
-_⋍_ : { a : T1 M A } { b : T1 M A } (f g  : T1Hom a b ) -> Set ℓ 
-_⋍_ {a} {b} f g = A [ T1Map f ≈ T1Map g ]
-infix 4 _⋍_ 
+MC :  Category (suc zero) c (suc (ℓ ⊔ c))
+MC = MONOID Mono
 
-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 )
-                    ; associative = IsCategory.associative (Category.isCategory A)
-                    }
-     where
-         open ≈-Reasoning (A) 
-         isEquivalence1 :  { a b : T1 M A } ->
-               IsEquivalence {_} {_} {T1Hom a b} _⋍_
-         isEquivalence1 {C} {D} =      -- this is the same function as A's equivalence but has different types
-           record { refl  = refl-hom
-             ; sym   = sym-hom
-             ; trans = trans-hom
-             } 
+open Monoid
+
+-- T : A -> (M x A)
 
-T1Category : Category  (ℓ ⊔ (c₂ ⊔ c₁))  (ℓ ⊔ (c₂ ⊔ c₁)) ℓ
-T1Category =
-  record { Obj = T1 M A
-         ; Hom = T1Hom
-         ; _o_ = _∘_
-         ; _≈_ = _⋍_
-         ; Id  = T1-id
-         ; isCategory = isT1Category
-         }
+T : Functor (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ })
+T = record {
+        FObj = \a -> (Carrier Mono) × a
+        ; FMap = \f -> map ( \x -> x ) f
+        ; isFunctor = record {
+             identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
+             ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
+             ; ≈-cong = cong1
+        } 
+    } where
+        cong1 : {ℓ′ : Level} -> {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} -> Sets [ f ≈ g ] → Sets [ map (λ x → x) f ≈ map (λ x → x) g ]
+        cong1 _≡_.refl = _≡_.refl
 
---  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 } ( 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 {
-        FObj = \a -> tobj a
-        ; FMap = tfmap
-        ; isFunctor = record
-        { ≈-cong   = ≈-cong
-             ; identity = identity1
-             ; distr    = distr1
-        }
-    } where
-        ≈-cong   : {a b : T1 M A} {f g : T1Hom a b} → f ⋍ g → tfmap f ⋍ tfmap g
-        ≈-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    = {!!}