# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376203929 -32400
# Node ID eb7ca6b9d3271b8fa06be64148cb972644c2c0aa
# Parent  5f331dfc000bdbc1f2d72d0b71ea03ce2acda4cd
trying..

diff -r 5f331dfc000b -r eb7ca6b9d327 cat-utility.agda
--- a/cat-utility.agda	Thu Aug 08 22:05:41 2013 +0900
+++ b/cat-utility.agda	Sun Aug 11 15:52:09 2013 +0900
@@ -70,10 +70,6 @@
 
         record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
                : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
-          eta : NTrans A A identityFunctor T
-          eta = η
-          mu : NTrans A A (T ○ T) T
-          mu = μ
           field
             isMonad : IsMonad A T η μ
              -- g ○ f = μ(c) T(g) f
diff -r 5f331dfc000b -r eb7ca6b9d327 monoid-monad.agda
--- a/monoid-monad.agda	Thu Aug 08 22:05:41 2013 +0900
+++ b/monoid-monad.agda	Sun Aug 11 15:52:09 2013 +0900
@@ -2,60 +2,43 @@
 open import Category.Monoid
 open import Algebra
 open import Level
-module monoid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ }  where
+module monoid-monad {c₁ c₂ ℓ : Level} { M : 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
-open import Data.Product
-open import Relation.Binary.Core
-open import Relation.Binary
-
-
-MC :  Category (suc zero) c (suc (ℓ ⊔ c))
-MC = MONOID Mono
 
 -- T : A -> (M x A)
+--    a -> m x a
+--    m x a -> m' x (m x a)
 
-T : ∀{ℓ′} -> Functor (Sets {ℓ′}) (Sets {ℓ ⊔  ℓ′} )
-T = record {
-        FObj = \a -> MS × 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
+data T1 {c₁ c₂ ℓ : Level}  (M :  Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( suc ( c₁ ⊔ c₂ ⊔ ℓ) ) where
+   T1a :  Obj A -> T1 M A
+   T1t :  Obj A -> T1 M A -> T1 M A
+
+T1HomMap : {c₁ c₂ ℓ : Level}  { A : Category c₁ c₂ ℓ }  {M :  Monoid c₁ ℓ }  (a : T1 {c₁} {c₂} {ℓ} M A ) (b : T1  {c₁} {c₂} {ℓ} M A) -> Set c₂ 
+T1HomMap {c₁} {c₂} {ℓ }  { A } (T1a a1 ) (T1a a2 ) = Hom A a1 a2
+T1HomMap {c₁} {c₂} {ℓ }  { A } (T1t a1 t1 ) (T1a a2 ) = Hom A a1 a2
+T1HomMap {c₁} {c₂} {ℓ }  { A } (T1a a1 ) (T1t a2 t2 ) = Hom A a1 a2
+T1HomMap {c₁} {c₂} {ℓ }  { A } (T1t a1 t1 ) (T1t a2 t2 ) = Hom A a1 a2
+
+record T1Hom1 {c₁ c₂ ℓ : Level}  { M : Monoid  c₁  ℓ}  { A : Category c₁ c₂ ℓ }  
+                 (a : T1 M A ) (b : T1 M A) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
+   field
+       T1Map  : T1HomMap a b
+
+open T1Hom1
+T1Hom = \(a b : T1 M A) -> T1Hom1 {c₁} {c₂} {ℓ} {M} {A} a b
+
+_*_ :  {c₁ c₂ ℓ : Level}  { A : Category c₁ c₂ ℓ }  {M :  Monoid c₁ ℓ } { a b c : T1 {c₁} {c₂} {ℓ } M A } -> T1Hom1  {c₁} {c₂} {ℓ} b c -> T1Hom1  {c₁} {c₂} {ℓ} a b -> T1Hom1  {c₁} {c₂} {ℓ} a c
+_*_ {c₁} {c₂} {ℓ } {A} {M} {a} {b} {c} g f  =  record { T1Map = A [ T1Map g  o T1Map f ] } 
 
 
--- Forgetful Functor
+
+
+
 
-open Functor 
-F : Functor MC Sets
-F  = record {
-        FObj = \a -> { s : Obj Sets } -> s 
-        ; FMap = \f -> ? -- {a : Obj Sets} { g : Hom Sets (FObj F *)  (FObj F ((Mor MC f) *)) } -> g
-        ; isFunctor = record {
-             identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
-             ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
---             ; ≈-cong = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets )))
-        } 
-    } 
+
 
--- Gerator
 
-G : Functor Sets MC
-G  = record {
-        FObj = \a -> * 
-        ; FMap = \f -> { g : Hom MC * * } -> Mor MC 
-        ; isFunctor = record {
-             identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory MC ))
-             ; distr = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory MC )))
-             ; ≈-cong = (IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory MC )))
-        } 
-    }