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)

open Monoid
Lemma-m01 : ( f g :  Carrier M ) ->  Carrier M
Lemma-m01 f g = _∙_  M f  g

data T1  (M :  Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( ( c₁ ⊔ c₂ ⊔ ℓ) ) where
   T1a :  Carrier M -> Obj A -> T1 M A
   T1t :  Carrier M -> T1 M A -> T1 M A 

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

T1M : (a : T1 M A )  -> Carrier M
T1M (T1a m _)  = m
T1M (T1t m _)  = m

tobj : ( a : T1 M A ) -> {m' : Carrier M } -> T1 M A
tobj (T1a m a)  {m'}  =  T1t m' ( T1a m a ) 
tobj (T1t m t)  {m'}  =  T1t m' ( T1t m t ) 

record T1Hom  (a : T1 M A ) (b : T1 M A) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
   field
       T1Map  : Hom A  (T1Obj a) (T1Obj b )
       P   : Hom A (T1Obj (tobj a {T1M a}) ) (T1Obj a)
       Q   : Hom A (T1Obj b ) (T1Obj (tobj b {T1M 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 ] ;
                      P     = P f;
                      Q     = Q g
    } 
infixr 9 _∘_ 


T1-id :  {a : T1 M A} → {p : Hom A (T1Obj (tobj a {T1M a}) ) (T1Obj a)} -> {q : Hom A (T1Obj a ) (T1Obj (tobj a {T1M a}) )} -> T1Hom a a
T1-id {a = a} {p} {q} = record { T1Map =  id1 A (T1Obj a) ; P = p; Q = q } 

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 =  isEquivalence1
                    ; 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) 
         isEquivalence1 :  { a b : T1 M A } ->
               IsEquivalence {_} {_} {T1Hom a b} _⋍_
         isEquivalence1 {C} {D} =      -- this is the same function as A's equivalence but has different types
           record { refl  = refl-hom
             ; sym   = sym-hom
             ; trans = trans-hom
             } 

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

--  T(f) (m,a)  = (m, f(a) )
--  T(f) = \(m,a)  -> (m, f(a) )
--  fmap f = T1 m a -> T1 m (f a)
tfmap : {a b : T1 M A } ( f : T1Hom a b ) -> T1Hom (tobj a {T1M a} ) (tobj b {T1M b} )
tfmap {a} {b} f =  record { T1Map = A [ Q f  o  A [ (T1Map f)  o P f ] ]  ;
                            P = ? ;
                            Q = ? 
   }

T : Functor T1Category T1Category
T = record {
        FObj = \a -> tobj a
        ; FMap = tfmap
        ; isFunctor = record
        { ≈-cong   = ≈-cong
             ; identity = identity1
             ; distr    = distr1
        }
    } where
        ≈-cong   : {a b : T1 M A} {f g : T1Hom a b} → f ⋍ g → tfmap f ⋍ tfmap g
        ≈-cong   = {!!}
        identity1 : {a : T1 M A} →  ((tfmap (T1-id {a} )) ⋍ (T1-id { tobj a })) 
        identity1 = {!!}
        distr1    :  {a b c : T1 M A} {f : T1Hom a b} {g : T1Hom b c} → 
                 ( tfmap ( g ∘ f) ⋍  ( tfmap g ∘ tfmap f ) )
        distr1    = {!!}