# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376365657 -32400
# Node ID 17f45f90977096e2e901bb649cfb8a59aef78d7f
# Parent  293e3e8c43dd718e563fa1268d21cb3f51781b88
η and μ defined.

diff -r 293e3e8c43dd -r 17f45f909770 monoid-monad.agda
--- a/monoid-monad.agda	Tue Aug 13 11:48:45 2013 +0900
+++ b/monoid-monad.agda	Tue Aug 13 12:47:37 2013 +0900
@@ -4,7 +4,6 @@
 open import Level
 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
@@ -19,18 +18,62 @@
 
 open Monoid
 
--- T : A -> (M x A)
+-- T : A → (M x A)
 
 T : Functor (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ })
 T = record {
-        FObj = \a -> (Carrier Mono) × a
-        ; FMap = \f -> map ( \x -> x ) f
+        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 : {ℓ′ : 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
 
+Lemma-MM1 :  {a b : Obj Sets} {f : Hom Sets a b} →
+        Sets [ Sets [ Functor.FMap T f o (λ x → ε Mono , x) ] ≈
+        Sets [ (λ x → ε Mono , x) o f ] ]
+Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in 
+        begin
+             Functor.FMap T f o (λ x → ε Mono , x)
+        ≈⟨⟩
+             (λ x → ε Mono , x) o f
+        ∎
+
+-- a → (ε,a)
+η : NTrans  (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) identityFunctor T
+η = record {
+       TMap = \a → \(x : a) → ( ε Mono , x ) ;
+       isNTrans = record {
+            commute = \{a} {b} {f} → IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
+       }
+  }
+
+-- (m,(m',a)) → (m*m,a)
+
+open Functor
+
+muMap : (a : Obj Sets  ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a )
+muMap a ( m , ( m' , x ) ) = ( _∙_ Mono m  m'  ,  x )
+
+Lemma-MM2 :  {a b : Obj Sets} {f : Hom Sets a b} →
+        Sets [ Sets [ FMap T f o (λ x → muMap a x) ] ≈
+        Sets [ (λ x → muMap b x) o FMap (T ○ T) f ] ]
+Lemma-MM2 {a} {b} {f} =  let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in                                                       
+        begin
+             FMap T f o (λ x → muMap a x)
+        ≈⟨⟩
+             (λ x → muMap b x) o FMap (T ○ T) f
+        ∎
+
+μ : NTrans  (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ( T ○ T ) T
+μ = record {
+       TMap = \a → \x  → muMap a x ; 
+       isNTrans = record {
+            commute = \{a} {b} {f} → IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
+       }
+  }