--- a/monoid-monad.agda	Thu Aug 15 12:32:48 2013 +0900
+++ b/monoid-monad.agda	Sat Aug 17 20:59:31 2013 +0900
@@ -24,7 +24,7 @@
     ε        : Carrier
     isMonoid : IsMonoid _≡_ _∙_ ε
 
-postulate Mono : ≡-Monoid c
+postulate M : ≡-Monoid c
 open ≡-Monoid
 
 A = Sets {c}
@@ -33,7 +33,7 @@
 
 T : Functor A A
 T = record {
-        FObj = λ a → (Carrier Mono) × a
+        FObj = λ a → (Carrier M) × a
         ; FMap = λ f → map ( λ x → x ) f
         ; isFunctor = record {
              identity = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
@@ -42,25 +42,25 @@
         } 
     } where
         cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} → 
-                   Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier Mono) → x) f ≈ map (λ (x : Carrier Mono) → x) g ]
+                   Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier M) → x) f ≈ map (λ (x : Carrier M) → x) g ]
         cong1 _≡_.refl = _≡_.refl
 
 open Functor
 
 Lemma-MM1 :  {a b : Obj A} {f : Hom A a b} →
-        A [ A [ FMap T f o (λ x → ε Mono , x) ] ≈
-        A [ (λ x → ε Mono , x) o f ] ]
+        A [ A [ FMap T f o (λ x → ε M , x) ] ≈
+        A [ (λ x → ε M , x) o f ] ]
 Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning A renaming ( _o_ to _*_ ) in 
         begin
-             FMap T f o (λ x → ε Mono , x)
+             FMap T f o (λ x → ε M , x)
         ≈⟨⟩
-             (λ x → ε Mono , x) o f
+             (λ x → ε M , x) o f
         ∎
 
 -- η : a → (ε,a)
 η : NTrans  A A identityFunctor T
 η = record {
-       TMap = λ a → λ(x : a) → ( ε Mono , x ) ;
+       TMap = λ a → λ(x : a) → ( ε M , x ) ;
        isNTrans = record {
             commute = Lemma-MM1
        }
@@ -68,8 +68,8 @@
 
 -- μ : (m,(m',a)) → (m*m,a)
 
-muMap : (a : Obj A  ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a )
-muMap a ( m , ( m' , x ) ) = ( _∙_ Mono m  m'  ,  x )
+muMap : (a : Obj A  ) → FObj T ( FObj T a ) → Σ (Carrier M) (λ x → a )
+muMap a ( m , ( m' , x ) ) = ( _∙_ M m  m'  ,  x )
 
 Lemma-MM2 :  {a b : Obj A} {f : Hom A a b} →
         A [ A [ FMap T f o (λ x → muMap a x) ] ≈
@@ -94,28 +94,28 @@
 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b}  {x :  Σ A B } →  (((proj₁ x) , proj₂ x ) ≡ x )
 Lemma-MM33 =  _≡_.refl
 
-Lemma-MM34 : ∀{ x : Carrier Mono  } → ( (Mono ∙ ε Mono) x ≡ x  )
-Lemma-MM34  {x} = (( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x )
+Lemma-MM34 : ∀{ x : Carrier M  } → ( (M ∙ ε M) x ≡ x  )
+Lemma-MM34  {x} = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x )
 
-Lemma-MM35 : ∀{ x : Carrier Mono  } → ((Mono ∙ x) (ε Mono))  ≡ x
-Lemma-MM35  {x} = ( proj₂  ( IsMonoid.identity ( isMonoid Mono )) ) x
+Lemma-MM35 : ∀{ x : Carrier M  } → ((M ∙ x) (ε M))  ≡ x
+Lemma-MM35  {x} = ( proj₂  ( IsMonoid.identity ( isMonoid M )) ) x
 
-Lemma-MM36 : ∀{ x y z : Carrier Mono } → ((Mono ∙ (Mono ∙ x) y) z)  ≡ (_∙_ Mono  x (_∙_ Mono y z ) )
-Lemma-MM36  {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono ))  x y z
+Lemma-MM36 : ∀{ x y z : Carrier M } → ((M ∙ (M ∙ x) y) z)  ≡ (_∙_ M  x (_∙_ M y z ) )
+Lemma-MM36  {x} {y} {z} = ( IsMonoid.assoc ( isMonoid M ))  x y z
 
 -- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming )
-postulate Extensionarity : {f g : Carrier Mono → Carrier Mono } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
+postulate Extensionarity : {f g : Carrier M → Carrier M } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 
 
-postulate Extensionarity3 : {f g : Carrier Mono → Carrier Mono → Carrier Mono → Carrier Mono } → 
+postulate Extensionarity3 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → 
                (∀{x y z} → f x y z ≡ g x y z )  → ( f ≡ g ) 
 
-Lemma-MM9  : ( λ(x : Carrier Mono) → ( Mono ∙ ε Mono ) x )  ≡ ( λ(x : Carrier Mono) → x ) 
+Lemma-MM9  : ( λ(x : Carrier M) → ( M ∙ ε M ) x )  ≡ ( λ(x : Carrier M) → x ) 
 Lemma-MM9  = Extensionarity Lemma-MM34
 
-Lemma-MM10 : ( λ x →   ((Mono ∙ x) (ε Mono)))  ≡ ( λ x → x ) 
+Lemma-MM10 : ( λ x →   ((M ∙ x) (ε M)))  ≡ ( λ x → x ) 
 Lemma-MM10 = Extensionarity Lemma-MM35
 
-Lemma-MM11 : (λ x y z → ((Mono ∙ (Mono ∙ x) y) z))  ≡ (λ x y z → ( _∙_ Mono  x (_∙_ Mono y z ) ))
+Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z))  ≡ (λ x y z → ( _∙_ M  x (_∙_ M y z ) ))
 Lemma-MM11 = Extensionarity3 Lemma-MM36 
 
 MonoidMonad : Monad A T η μ 
@@ -131,7 +131,7 @@
                 begin
                      TMap μ a o TMap η ( FObj T a )
                 ≈⟨⟩
-                    ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
+                    ( λ x → ((M ∙ ε M) (proj₁ x) , proj₂ x ))
                 ≈⟨  cong ( λ f → ( λ x →  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
                     ( λ (x : FObj T a) → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
@@ -144,7 +144,7 @@
                 begin
                      TMap μ a o (FMap T (TMap η a ))
                 ≈⟨⟩
-                    ( λ x → (Mono ∙ proj₁ x) (ε Mono) , proj₂ x )
+                    ( λ x → (M ∙ proj₁ x) (ε M) , proj₂ x )
                 ≈⟨  cong ( λ f → ( λ x →  ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 )  ⟩
                     ( λ x → (proj₁ x) , proj₂ x )
                 ≈⟨⟩
@@ -157,14 +157,26 @@
                 begin
                       TMap μ a o TMap μ ( FObj T a ) 
                 ≈⟨⟩
-                      ( λ x → (Mono ∙ (Mono ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x)))
+                      ( λ x → (M ∙ (M ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x)))
                 ≈⟨ cong ( λ f → ( λ x → 
                          (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x)))  )) ,  proj₂ (proj₂ (proj₂ x)) )
                          )) Lemma-MM11  ⟩
-                      ( λ x → (Mono ∙ proj₁ x) ((Mono ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
+                      ( λ x → (M ∙ proj₁ x) ((M ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
                 ≈⟨⟩
                       TMap μ a o FMap T (TMap μ a)
                 ∎
 
 
+F  : (m : Carrier M) -> { a b : Obj A } -> ( f : a -> b ) -> Hom A a ( FObj T b )
+F m {a} {b} f =  \(x : a ) -> ( m , ( f x) )
 
+postulate m m' : Carrier M
+postulate a b c' : Obj A 
+postulate f :  b -> c'
+postulate g :  a -> b
+
+LemmaMM12 =  Monad.join MonoidMonad (F m f) (F m' g)
+
+open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad}
+
+