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