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  (M :  Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( ( c₁ ⊔ c₂ ⊔ ℓ) ) where
   T1a :  Obj A -> T1 M A
   T1t :  Obj A -> T1 M A -> T1 M A

T1Obj : (a : T1 M A )  -> Obj A
T1Obj (T1a a1 )  = a1
T1Obj (T1t a1 t1 )  = a1

record T1Hom  (a : T1 M A ) (b : T1 M A) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
   field
       T1Map  : Hom A  (T1Obj a) (T1Obj b )

open T1Hom
_∙_ :  { a b c : T1 M A } -> T1Hom b c -> T1Hom a b -> T1Hom  a c
_∙_  g f  =  record { T1Map = A [ T1Map g  o T1Map f ] } 
infixr 9 _∙_ 


T1-id :  {a : T1 M A} → T1Hom a a
T1-id {a = a} = record { T1Map =  id1 A (T1Obj a) } 

open import Relation.Binary.Core

_⋍_ : { a : T1 M A } { b : T1 M A } (f g  : T1Hom a b ) -> Set ℓ 
_⋍_ {a} {b} f g = A [ T1Map f ≈ T1Map g ]
infix 4 _⋍_ 

isT1Category : IsCategory ( T1 M A ) T1Hom _⋍_ _∙_ T1-id 
isT1Category  = record  { isEquivalence =  isEquivalence 
                    ; identityL =   IsCategory.identityL (Category.isCategory A)
                    ; identityR =   IsCategory.identityR (Category.isCategory A)
                    ; o-resp-≈ =    IsCategory.o-resp-≈ ( Category.isCategory A )
                    ; associative = IsCategory.associative (Category.isCategory A)
                    }
     where
         open ≈-Reasoning (A) 
         isEquivalence :  { a b : T1 M A } ->
               IsEquivalence {_} {_} {T1Hom a b} _⋍_
         isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
           record { refl  = refl-hom
             ; sym   = sym
             ; trans = trans-hom
             } 

T1Category : Category  (ℓ ⊔ (c₂ ⊔ c₁))  (ℓ ⊔ (c₂ ⊔ c₁)) ℓ
T1Category =
  record { Obj = T1 M A
         ; Hom = T1Hom
         ; _o_ = _∙_
         ; _≈_ = _⋍_
         ; Id  = T1-id
         ; isCategory = isT1Category
         }