open import Category -- https://github.com/konn/category-agda                                                                                     
open import Algebra
open import Level
open import Category.Sets
module monoid-monad {c : Level} where

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

-- open Monoid
open import Algebra.FunctionProperties using (Op₁; Op₂)


record ≡-Monoid c : Set (suc c) where
  infixl 7 _∙_
  field
    Carrier  : Set c
    _∙_      : Op₂ Carrier
    ε        : Carrier
    isMonoid : IsMonoid _≡_ _∙_ ε

postulate Mono : ≡-Monoid c
open ≡-Monoid

A = Sets {c}

-- T : A → (M x A)

T : Functor A A
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 : Carrier Mono) → x) f ≈ map (λ (x : Carrier Mono) → x) g ]
        cong1 _≡_.refl = _≡_.refl

open Functor

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

-- η : a → (ε,a)
η : NTrans  A A identityFunctor T
η = record {
       TMap = λ a → λ(x : a) → ( ε Mono , x ) ;
       isNTrans = record {
            commute = Lemma-MM1
       }
  }

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

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

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

μ : NTrans  A A ( T ○ T ) T
μ = record {
       TMap = λ a → λ x  → muMap a x ; 
       isNTrans = record {
            commute = λ{a} {b} {f} → Lemma-MM2 {a} {b} {f}
       }
  }

open NTrans

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-MM34 : ∀{ x : Carrier Mono  } → ( (Mono ∙ ε Mono) x ≡ x  )
Lemma-MM34  {x} = (( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x )

Lemma-MM35 : ∀{ x : Carrier Mono  } → ((Mono ∙ x) (ε Mono))  ≡ x
Lemma-MM35  {x} = ( proj₂  ( IsMonoid.identity ( isMonoid Mono )) ) x

Lemma-MM36 : ∀{ x y z : Carrier Mono } → ((Mono ∙ (Mono ∙ x) y) z)  ≡ (_∙_ Mono  x (_∙_ Mono y z ) )
Lemma-MM36  {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono ))  x y z

-- Functional Extensionarity Axiom (We cannot prove this in Agda / Coq, just assumming )
postulate Extensionarity : {f g : Carrier Mono → Carrier Mono } → (∀ {x} → (f x ≡ g x))  → ( f ≡ g ) 

postulate Extensionarity3 : {f g : Carrier Mono → Carrier Mono → Carrier Mono → Carrier Mono } → 
               (∀{x y z} → f x y z ≡ g x y z )  → ( f ≡ g ) 

Lemma-MM9  : ( λ(x : Carrier Mono) → ( Mono ∙ ε Mono ) x )  ≡ ( λ(x : Carrier Mono) → x ) 
Lemma-MM9  = Extensionarity Lemma-MM34

Lemma-MM10 : ( λ x →   ((Mono ∙ x) (ε Mono)))  ≡ ( λ x → x ) 
Lemma-MM10 = Extensionarity Lemma-MM35

Lemma-MM11 : (λ x y z → ((Mono ∙ (Mono ∙ x) y) z))  ≡ (λ x y z → ( _∙_ Mono  x (_∙_ Mono y z ) ))
Lemma-MM11 = Extensionarity3 Lemma-MM36 

MonoidMonad : Monad A T η μ 
MonoidMonad = record {
       isMonad = record {
           unity1 = Lemma-MM3 ;
           unity2 = Lemma-MM4 ;
           assoc  = Lemma-MM5 
       }  
   } where
       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 (A) renaming ( _o_ to _*_ ) in
                begin
                     TMap μ a o TMap η ( FObj T a )
                ≈⟨⟩
                    ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
                ≈⟨  cong ( λ f → ( λ x →  ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 )  ⟩
                    ( λ (x : FObj T a) → (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 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
                begin
                     TMap μ a o (FMap T (TMap η a ))
                ≈⟨⟩
                    ( λ x → (Mono ∙ proj₁ x) (ε Mono) , proj₂ x )
                ≈⟨  cong ( λ f → ( λ x →  ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 )  ⟩
                    ( λ x → (proj₁ x) , proj₂ x )
                ≈⟨⟩
                    ( λ x → x )
                ≈⟨⟩
                     Id {_} {_} {_} {A} (FObj T a)
                ∎
       Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
       Lemma-MM5 {a} = let open ≈-Reasoning (A) renaming ( _o_ to _*_ ) in
                begin
                      TMap μ a o TMap μ ( FObj T a ) 
                ≈⟨⟩
                      ( λ x → (Mono ∙ (Mono ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x)))
                ≈⟨ cong ( λ f → ( λ x → 
                         (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x)))  )) ,  proj₂ (proj₂ (proj₂ x)) )
                         )) Lemma-MM11  ⟩
                      ( λ x → (Mono ∙ proj₁ x) ((Mono ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x)))
                ≈⟨⟩
                      TMap μ a o FMap T (TMap μ a)
                ∎