--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/monoid-monad.agda	Sat Aug 03 10:12:00 2013 +0900
@@ -0,0 +1,37 @@
+open import Category -- https://github.com/konn/category-agda                                                                                     
+open import Level
+--open import Category.HomReasoning                                                                                                               
+open import HomReasoning
+open import cat-utility
+open import Category.Cat
+open import Category.Sets
+open import Algebra
+open import Category.Monoid
+open import Data.Product
+open import Relation.Binary.Core
+open import Relation.Binary
+
+module monooid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ }  where
+
+
+MC :  Category (suc zero) c (suc (ℓ ⊔ c))
+MC = MONOID Mono
+
+-- T : A -> (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
+
+
+
+