open import Category -- https://github.com/konn/category-agda                                                                                     
open import Category.Monoid
open import Algebra
open import Level
module monoid-monad {c₁ c₂ ℓ : Level} { M : Monoid c₁ ℓ} {A : Category c₁ c₂ ℓ }  where

open import HomReasoning
open import cat-utility
open import Category.Cat
open import Category.Sets

-- T : A -> (M x A)
--    a -> m x a
--    m x a -> m' x (m x a)

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 ] }