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

open import Algebra.Structures
open import HomReasoning
open import cat-utility
open import Category.Cat
open import Category.Sets
open import Data.Product
open import Relation.Binary.Core
open import Relation.Binary

open Monoid

-- T : A → (M x A)

T : Functor (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ })
T = record {
        FObj = \a → (Carrier Mono) × 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

Lemma-MM1 :  {a b : Obj Sets} {f : Hom Sets a b} →
        Sets [ Sets [ Functor.FMap T f o (λ x → ε Mono , x) ] ≈
        Sets [ (λ x → ε Mono , x) o f ] ]
Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in 
        begin
             Functor.FMap T f o (λ x → ε Mono , x)
        ≈⟨⟩
             (λ x → ε Mono , x) o f
        ∎

-- a → (ε,a)
η : NTrans  (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) identityFunctor T
η = record {
       TMap = \a → \(x : a) → ( ε Mono , x ) ;
       isNTrans = record {
            commute = \{a} {b} {f} → IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
       }
  }

-- (m,(m',a)) → (m*m,a)

open Functor

muMap : (a : Obj Sets  ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a )
muMap a ( m , ( m' , x ) ) = ( _∙_ Mono m  m'  ,  x )

Lemma-MM2 :  {a b : Obj Sets} {f : Hom Sets a b} →
        Sets [ Sets [ FMap T f o (λ x → muMap a x) ] ≈
        Sets [ (λ x → muMap b x) o FMap (T ○ T) f ] ]
Lemma-MM2 {a} {b} {f} =  let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in                                                       
        begin
             FMap T f o (λ x → muMap a x)
        ≈⟨⟩
             (λ x → muMap b x) o FMap (T ○ T) f
        ∎

μ : NTrans  (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ( T ○ T ) T
μ = record {
       TMap = \a → \x  → muMap a x ; 
       isNTrans = record {
            commute = \{a} {b} {f} → IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))
       }
  }

open NTrans

Lemma-MM32 :  ∀{ℓ} {a : Set ℓ } -> {f g : a -> a } -> {x : a } -> ( f ≡ g ) -> ( ( λ x → f x )  ≡ ( λ x → g x ) )
Lemma-MM32 eq = cong ( \f -> \x -> f x  ) eq

Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b}  {x :  Σ A B } →  (((proj₁ x) , proj₂ x ) ≡  x )
Lemma-MM33 =  _≡_.refl

Lemma-M-34 : ( x : Carrier Mono  ) -> _≈_ Mono ((_∙_ Mono (ε Mono)  x)) x 
Lemma-M-34  = proj₁ ( IsMonoid.identity ( isMonoid Mono ) )

Lemma-MM31 : ( a : Obj ( Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ) -> {x : FObj T a } →  (((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ) ≡  x )
Lemma-MM31 a = {!!}

MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ 
MonoidMonad = record {
       isMonad = record {
           unity1 =  \{a} -> Lemma-MM3 {a} ;
           unity2 = Lemma-MM4 ;
           assoc = Lemma-MM5 
       }  
   } where
       A = Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ } 
       Lemma-MM3 :  {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
       Lemma-MM3 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
                begin
                     TMap μ a o TMap η ( FObj T a )
                ≈⟨⟩
                    ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
                ≈⟨ {!!} ⟩
                    ( λ x → x )
                ≈⟨⟩
                     Id {_} {_} {_} {A} (FObj T a)
                ∎
       Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
       Lemma-MM4 = {!!}
       Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
       Lemma-MM5 = {!!}