-- Monad
-- Category A
-- A = Category
-- Functor T : A → A
--T(a) = t(a)
--T(f) = tf(f)

open import Category -- https://github.com/konn/category-agda
open import Level
--open import Category.HomReasoning
open import HomReasoning
open import cat-utility
open import Category.Cat

module nat { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { M : Monad A T η μ } 
                 { K : Kleisli A T η μ M } where


--T(g f) = T(g) T(f)

open Functor
Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) →  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
     → A [ ( FMap T (A [ g o f ] ))  ≈ (A [ FMap T g o FMap T f ]) ]
Lemma1 = \t → IsFunctor.distr ( isFunctor t )


open NTrans
Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} 
      → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b }
      → A [ A [  FMap G f o TMap μ a ]  ≈ A [ TMap μ b o  FMap F f ] ]
Lemma2 = \n → IsNTrans.naturality ( isNTrans  n  )

-- η :   1_A → T
-- μ :   TT → T
-- μ(a)η(T(a)) = a
-- μ(a)T(η(a)) = a
-- μ(a)(μ(T(a))) = μ(a)T(μ(a))


open Monad
Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { a : Obj A } →
                 ( M : Monad A T η μ )
    → A [ A [  TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
Lemma3 = \m → IsMonad.assoc ( isMonad m )


Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
    → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
Lemma4 = \a → IsCategory.identityL ( Category.isCategory a )

Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { a : Obj A } →
                 ( M : Monad A T η μ )
    →  A [ A [ TMap μ a o TMap η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
Lemma5 = \m → IsMonad.unity1 ( isMonad m )

Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { a : Obj A } →
                 ( M : Monad A T η μ )
    →  A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
Lemma6 = \m → IsMonad.unity2 ( isMonad m )

-- T = M x A
-- nat of η
-- g ○ f = μ(c) T(g) f
-- η(b) ○ f = f
-- f ○ η(a) = f
-- h ○ (g ○ f) = (h ○ g) ○ f


lemma12 :  {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → 
       ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ]
lemma12 L x y =  
   let open ≈-Reasoning ( L )  in 
      begin  L [ x o y ]  ∎

open Kleisli
-- η(b) ○ f = f
Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) )
                      → A  [ join K (TMap η b) f  ≈ f ]
Lemma7 {_} {b} f = 
  let open ≈-Reasoning (A) in 
     begin  
         join K (TMap η b) f 
     ≈⟨ refl-hom ⟩
         A [ TMap μ b  o A [ FMap T ((TMap η b)) o f ] ]  
     ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
        A [ A [ TMap μ b  o  FMap T ((TMap η b)) ] o f ]
     ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad K )) )  ⟩
        A [  id (FObj T b)   o f ]
     ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩
        f
     ∎

-- f ○ η(a) = f
Lemma8 : { a  : Obj A }  { b : Obj A }
                 ( f : Hom A a ( FObj T b) )
                      → A  [ join K f (TMap η a)  ≈ f ]
Lemma8 {a} {b} f = 
  begin
     join K f (TMap η a) 
  ≈⟨ refl-hom ⟩
     A [ TMap μ b  o A [  FMap T f o (TMap η a) ] ]  
  ≈⟨ cdr  ( nat η ) ⟩
     A [ TMap μ b  o A [ (TMap η ( FObj T b)) o f ] ] 
  ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
     A [ A [ TMap μ b  o (TMap η ( FObj T b)) ] o f ] 
  ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad K )) ) ⟩
     A [ id (FObj T b)  o f ]
  ≈⟨  IsCategory.identityL (Category.isCategory A)  ⟩
     f
  ∎  where 
      open ≈-Reasoning (A) 

-- h ○ (g ○ f) = (h ○ g) ○ f
Lemma9 : { a b c d : Obj A }
                 ( h : Hom A c ( FObj T d) )
                 ( g : Hom A b ( FObj T c) ) 
                 ( f : Hom A a ( FObj T b) )
                      → A  [ join K h (join K g f)  ≈ join K ( join K h g) f ]
Lemma9 {a} {b} {c} {d} h g f = 
  begin 
     join K h (join K g f)  
   ≈⟨⟩
     join K h (                  ( TMap μ c o ( FMap T g o f ) ) )
   ≈⟨ refl-hom ⟩
     ( TMap μ d  o ( FMap T h  o  ( TMap μ c o ( FMap T g  o f ) ) ) )
   ≈⟨ cdr ( cdr ( assoc )) ⟩
     ( TMap μ d  o ( FMap T h o ( ( TMap μ c o  FMap T g )  o f ) ) )
   ≈⟨ assoc  ⟩    ---   ( f  o  ( g  o  h ) ) = ( ( f  o  g )  o  h )
     (     ( TMap μ d o  FMap T h ) o  ( (TMap μ c   o  FMap T g )    o f ) )
   ≈⟨ assoc  ⟩
     ( ( ( TMap μ d o      FMap T h ) o  (TMap μ c   o  FMap T g ) )  o f )
   ≈⟨ car (sym assoc) ⟩
     ( ( TMap μ d o  ( FMap T h     o   ( TMap μ c   o  FMap T g ) ) ) o f )
   ≈⟨ car ( cdr (assoc) ) ⟩
     ( ( TMap μ d o  ( ( FMap T h o       TMap μ c ) o  FMap T g )   ) o f )
   ≈⟨ car assoc ⟩
     ( ( ( TMap μ d o  ( FMap T h   o   TMap μ c ) ) o  FMap T g ) o f )
   ≈⟨ car (car ( cdr ( begin 
           ( FMap T h o TMap μ c )
       ≈⟨ nat μ ⟩
           ( TMap μ (FObj T d) o FMap T (FMap T h) )
        ∎ 
   )))  ⟩
      ( ( ( TMap μ d  o  ( TMap μ ( FObj T d)  o FMap T (  FMap T h ) ) )  o FMap T g )  o f )
   ≈⟨ car (sym assoc) ⟩
     ( ( TMap μ d  o  ( ( TMap μ ( FObj T d)   o FMap T (  FMap T h ) )   o FMap T g ) )   o f )
   ≈⟨ car ( cdr (sym assoc) ) ⟩
     ( ( TMap μ d  o  ( TMap μ ( FObj T d)   o ( FMap T (  FMap T h ) o FMap T g ) ) )   o f )
   ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩
     ( ( TMap μ d  o  ( TMap μ ( FObj T d)     o FMap T ( ( FMap T h  o g ) ) ) )   o f )
   ≈⟨ car assoc ⟩
     ( ( ( TMap μ d  o  TMap μ ( FObj T d)  )  o FMap T ( ( FMap T h  o g ) ) )    o f )
   ≈⟨ car ( car (
      begin
         ( TMap μ d o TMap μ (FObj T d) )
      ≈⟨ IsMonad.assoc ( isMonad M) ⟩
         ( TMap μ d o FMap T (TMap μ d) )
      ∎
   )) ⟩
     ( ( ( TMap μ d  o    FMap T ( TMap μ d) ) o FMap T ( ( FMap T h  o g ) ) )    o f )
   ≈⟨ car (sym assoc) ⟩
     ( ( TMap μ d  o  ( FMap T ( TMap μ d )    o FMap T ( ( FMap T h  o g ) ) ) )  o f )
   ≈⟨ sym assoc ⟩
     ( TMap μ d  o  ( ( FMap T ( TMap μ d )    o FMap T ( ( FMap T h  o g ) ) )  o f ) )
   ≈⟨ cdr ( car ( sym ( distr T )))   ⟩
     ( TMap μ d  o ( FMap T ( ( ( TMap μ d )   o ( FMap T h  o g ) ) ) o f ) )
   ≈⟨ refl-hom ⟩
     join K ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
   ≈⟨ refl-hom ⟩
     join K ( join K h g) f 
  ∎ where open ≈-Reasoning (A) 

Lemma10 :  {a b c : Obj A} -> (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → 
                          A [ f ≈ g ] → A [ h ≈ i ] → A [ (join K h f) ≈ (join K i g) ]
Lemma10 {a} {b} {c} f g h i eq-fg eq-hi = let open ≈-Reasoning (A) in
   begin 
       join K h f
   ≈⟨⟩
       TMap μ c  o ( FMap T h  o f )
   ≈⟨ cdr ( IsCategory.o-resp-≈ (Category.isCategory A) eq-fg ((IsFunctor.≈-cong (isFunctor T)) eq-hi )) ⟩
       TMap μ c  o ( FMap T i  o g )
   ≈⟨⟩
       join K i g
   ∎


record KHom (a : Obj A)  (b : Obj A)
     : Set (suc (c₂ ⊔ c₁)) where
   field
       KMap :  Hom A a ( FObj T b )

K-id :  {a : Obj A} → KHom a a
K-id {a = a} = record { KMap =  TMap η a } 

open import Relation.Binary.Core
open KHom

_⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ 
_⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]

_*_ : { a b : Obj A } → { c : Obj A } →
                      ( KHom b c) → (  KHom a b) → KHom a c 
_*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) }

isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id 
isKleisliCategory  = record  { isEquivalence =  isEquivalence 
                    ; identityL =   KidL
                    ; identityR =   KidR
                    ; o-resp-≈ =    Ko-resp
                    ; associative = Kassoc
                    }
     where
         open ≈-Reasoning (A) 
         isEquivalence :  { a b : Obj A } ->
               IsEquivalence {_} {_} {KHom a b} _⋍_
         isEquivalence {C} {D} =
           record { refl  = λ {F} → ⋍-refl {F}
             ; sym   = λ {F} {G} → ⋍-sym {F} {G}
             ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H}
             } where
                  ⋍-refl : {F : KHom C D} → F ⋍ F
                  ⋍-refl = refl-hom
                  ⋍-sym : {F G : KHom C D} → F ⋍ G → G ⋍ F
                  ⋍-sym = sym
                  ⋍-trans : {F G H : KHom C D} → F ⋍ G → G ⋍ H → F ⋍ H
                  ⋍-trans = trans-hom
         KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f
         KidL {_} {_} {f} =  Lemma7 (KMap f) 
         KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f
         KidR {_} {_} {f} =  Lemma8 (KMap f) 
         Ko-resp :  {a b c : Obj A} -> {f g : KHom a b } → {h i : KHom  b c } → 
                          f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
         Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = Lemma10 {a} {b} {c} (KMap f) (KMap g) (KMap h) (KMap i) eq-fg eq-hi
         Kassoc :   {a b c d : Obj A} -> {f : KHom c d } → {g : KHom b c } → {h : KHom a b } →
                          (f * (g * h)) ⋍ ((f * g) * h)
         Kassoc {_} {_} {_} {_} {f} {g} {h} =  Lemma9 (KMap f) (KMap g) (KMap h) 

KleisliCategory : Category c₁ (suc (c₂ ⊔ c₁)) ℓ
KleisliCategory =
  record { Obj = Obj A
         ; Hom = KHom
         ; _o_ = _*_
         ; _≈_ = _⋍_
         ; Id  = K-id
         ; isCategory = isKleisliCategory
         }

U_T : Functor KleisliCategory A
U_T = record {
        FObj = FObj T
          ; FMap = ufmap
        ; isFunctor = record
        {      ≈-cong   = ≈-cong
             ; identity = identity
             ; distr    = distr1
        }
     } where
        ufmap : {a b : Obj A} (f : KHom a b ) -> Hom A (FObj T a) (FObj T b)
        ufmap {a} {b} f =  A [ TMap μ (b)  o FMap T (KMap f) ]
        identity : {a : Obj A} →  A [ ufmap (K-id {a}) ≈ id1 A (FObj T a) ]
        identity {a} = let open ≈-Reasoning (A) in
          begin
              TMap μ (a)  o FMap T (TMap η a)
          ≈⟨ IsMonad.unity2 (isMonad M) ⟩
             id1 A (FObj T a)
          ∎
        ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ]
        ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
          begin
             TMap μ (b)  o FMap T (KMap f)
          ≈⟨ cdr (fcong T f≈g) ⟩
             TMap μ (b)  o FMap T (KMap g)
          ∎
        distr1 :  {a b c : Obj A} {f : KHom a b} {g : KHom b c} → A [ ufmap (g * f) ≈ (A [ ufmap g o ufmap f ] )]
        distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in
          begin
             ufmap (g * f)
          ≈⟨⟩
             ufmap {a} {c} ( record { KMap = TMap μ (c) o (FMap T (KMap g)  o (KMap f)) } )
          ≈⟨⟩
             TMap μ (c)  o  FMap T ( TMap μ (c) o (FMap T (KMap g)  o (KMap f)))
          ≈⟨ cdr ( distr T) ⟩
             TMap μ (c)  o (( FMap T ( TMap μ (c)) o FMap T  (FMap T (KMap g)  o (KMap f))))
          ≈⟨ assoc ⟩
             (TMap μ (c)  o ( FMap T ( TMap μ (c)))) o FMap T  (FMap T (KMap g)  o (KMap f))
          ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩
             (TMap μ (c)  o ( TMap μ (FObj T c))) o FMap T  (FMap T (KMap g)  o (KMap f))
          ≈⟨ sym assoc ⟩
             TMap μ (c)  o (( TMap μ (FObj T c)) o FMap T  (FMap T (KMap g)  o (KMap f)))
          ≈⟨ cdr (cdr (distr T)) ⟩
             TMap μ (c)  o (( TMap μ (FObj T c)) o (FMap T  (FMap T (KMap g))  o FMap T (KMap f)))
          ≈⟨ cdr (assoc) ⟩
             TMap μ (c)  o ((( TMap μ (FObj T c)) o (FMap T  (FMap T (KMap g))))  o FMap T (KMap f))
          ≈⟨ sym (cdr (car (nat μ ))) ⟩
             TMap μ (c)  o ((FMap T (KMap g )  o  TMap μ (b))  o FMap T (KMap f ))
          ≈⟨ cdr (sym assoc) ⟩
             TMap μ (c)  o (FMap T (KMap g )  o  ( TMap μ (b)  o FMap T (KMap f )))
          ≈⟨ assoc ⟩
             ( TMap μ (c)  o FMap T (KMap g ) )  o  ( TMap μ (b)  o FMap T (KMap f ) )
          ≈⟨⟩
             ufmap g o ufmap f
          ∎


ffmap :  {a b : Obj A} (f : Hom A a b) -> KHom a b
ffmap f = record { KMap = A [ TMap η (Category.cod A f) o f ] }

F_T : Functor A KleisliCategory
F_T = record {
        FObj = \a -> a
        ; FMap = ffmap
        ; isFunctor = record
        { ≈-cong   = ≈-cong
             ; identity = identity
             ; distr    = distr1
        }
     } where
        identity : {a : Obj A} →  A [ A [ TMap η a o id1 A a ] ≈ TMap η a  ]
        identity {a} = IsCategory.identityR ( Category.isCategory A)
        lemma1 : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ TMap η b  ≈  TMap η b ]
        lemma1 f≈g = IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))
        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → A [ A [ TMap η (Category.cod A f) o f ] ≈ A [ TMap η (Category.cod A g) o g ] ]
        ≈-cong f≈g =  (IsCategory.o-resp-≈ (Category.isCategory A)) f≈g ( lemma1  f≈g )
        distr1 :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → 
                 ( ffmap (A [ g o f ]) ⋍  ( ffmap g * ffmap f ) )
        distr1 {_} {_} {_} {f} {g} =  let open ≈-Reasoning (A) in
          begin
             KMap (ffmap (A [ g o f ]))
          ≈⟨ {!!} ⟩
             KMap  ( ffmap g * ffmap f )
          ∎