module nat  where 

-- 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

--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  )

open import Category.Cat

-- η :   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 : {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 } ( b : Obj A ) 
                 ( f : Hom A a ( FObj T b) )
                 ( m : Monad A T η μ )
                 { k : Kleisli A T η μ m}
                      → A  [ join k b (TMap η b) f  ≈ f ]
Lemma7 c {T} η b f m {k} = 
  let open ≈-Reasoning (c) 
      μ = mu ( monad k )
  in 
     begin  
         join k b (TMap η b) f 
     ≈⟨ refl-hom ⟩
         c [ TMap μ b  o c [ FMap T ((TMap η b)) o f ] ]  
     ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
        c [ c [ TMap μ b  o  FMap T ((TMap η b)) ] o f ]
     ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) )  ⟩
        c [  id (FObj T b)   o f ]
     ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
        f
     ∎

-- f ○ η(a) = f
Lemma8 : {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 )  ( b : Obj A )
                 ( f : Hom A a ( FObj T b) )
                 ( m : Monad A T η μ )
                 ( k : Kleisli A T η μ m) 
                      → A  [ join k b f (TMap η a)  ≈ f ]
Lemma8 c T η a b f m k = 
  begin
     join k b f (TMap η a) 
  ≈⟨ refl-hom ⟩
     c [ TMap μ b  o c [  FMap T f o (TMap η a) ] ]  
  ≈⟨ cdr  ( nat η ) ⟩
     c [ TMap μ b  o c [ (TMap η ( FObj T b)) o f ] ] 
  ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
     c [ c [ TMap μ b  o (TMap η ( FObj T b)) ] o f ] 
  ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩
     c [ id (FObj T b)  o f ]
  ≈⟨  IsCategory.identityL (Category.isCategory c)  ⟩
     f
  ∎  where 
      open ≈-Reasoning (c) 
      μ = mu ( monad k )

-- h ○ (g ○ f) = (h ○ g) ○ f
Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { a b c d : Obj A }
                 ( f : Hom A a ( FObj T b) )
                 ( g : Hom A b ( FObj T c) ) 
                 ( h : Hom A c ( FObj T d) )
                 ( m : Monad A T η μ )
                 { k : Kleisli A T η μ m}
                      → A  [ join k d h (join k c g f)  ≈ join k d ( join k d h g) f ]
Lemma9 A {T} {η} {μ} {a} {b} {c} {d} f g h m {k} = 
  begin 
     join k d h (join k c g f)  
   ≈⟨⟩
     join k d 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 d ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
   ≈⟨ refl-hom ⟩
     join k d ( join k d h g) f 
  ∎ where open ≈-Reasoning (A) 

-- Kleisli-join : {!!}
-- Kleisli-join = {!!}

-- Kleisli-id : {!!}
-- Kleisli-id = {!!}

-- Lemma10 : {!!}
-- Lemma10 = {!!}

-- open import Relation.Binary.Core

-- isKleisliCategory : {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} →
--          IsCategory ( Obj A ) ( Hom A ) ( Category._≈_ A ) ( Kleisli-join ) Kleisli-id
-- isKleisliCategory A {T} {η} m = record  { isEquivalence =  IsCategory.isEquivalence ( Category.isCategory A )
--                     ; identityL =   {!!}
--                     ; identityR =   {!!}
--                     ; o-resp-≈ =    {!!}
--                     ; associative = {!!}
--                     }
--      where
--          KidL : {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 η μ ) → {!!}
--          KidL = {!!}
--          KidR : {!!}
--          KidR = {!!}
--          Ko-resp : {!!}
--          Ko-resp = {!!}
--          Kassoc : {!!}
--          Kassoc = {!!}

-- Kleisli :
-- Kleisli = record { Hom = 
--                 ; Hom = _⟶_
--                  ; Id = IdProd
--                  ; _o_ = _∘_
--                  ; _≈_ = _≈_
--                  ; isCategory = record { isEquivalence = record { refl  = λ {φ} → ≈-refl {φ = φ}
--                                                                 ; sym   = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
--                                                                 ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
--                                                                 }
--                                        ; identityL = identityL
--                                        ; identityR = identityR
--                                        ; o-resp-≈ = o-resp-≈
--                                        ; associative = associative
--                                        }
--                  }

----
--
-- Adjunction to Monad
--
----

open Adjunction

UεF :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                 ( U : Functor B A )
                 ( F : Functor A B )
                 ( ε : NTrans B B  ( F ○  U ) identityFunctor ) → NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
UεF A B U F ε =  lemma11  (
     Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○  U} {identityFunctor} ε F)  ) where
         lemma11 :   NTrans A A   ( U ○ ((F  ○  U) ○  F )) ( U ○  (identityFunctor ○ F) ) 
                  →  NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
         lemma11  n = record { TMap = \a → TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }}

Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
                 { U : Functor B A }
                 { F : Functor A B }
                 { η : NTrans A A identityFunctor ( U ○  F ) }
                 { ε : NTrans B B  ( F ○  U ) identityFunctor } →
      Adjunction A B U F η ε  → Monad A (U ○  F) η (UεF A B U F ε)
Adj2Monad A B {U} {F} {η} {ε} adj = record {
         isMonad = record {
                    assoc = assoc1;
                    unity1 = unity1;
                    unity2 = unity2
              }
      }  where
           T : Functor A A
           T = U  ○ F
           μ : NTrans A A ( T ○ T ) T
           μ = UεF A B U F ε
           lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) → 
                 B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ] 
           lemma-assoc1 f =  IsNTrans.naturality ( isNTrans ε )
           assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
           assoc1 {a} = let open ≈-Reasoning (A) in
             begin
                TMap μ a o TMap μ ( FObj T a )
             ≈⟨⟩
                (FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F  a )))))
             ≈⟨ sym (distr U) ⟩
                FMap U (B [ TMap ε ( FObj F a )  o TMap ε ( FObj F ( FObj U (FObj F a ))) ] )
             ≈⟨  (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩
                FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] )
             ≈⟨ distr U ⟩
                (FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a ))))
             ≈⟨⟩
                TMap μ a o FMap T (TMap μ a) 
             ∎
           unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
           unity1 {a} = let open ≈-Reasoning (A) in
             begin
               TMap μ a o TMap η ( FObj T a )
             ≈⟨⟩
               (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F  a ))
             ≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩
               id (FObj U ( FObj F a ))
             ≈⟨⟩
               id (FObj T a)
             ∎
           unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
           unity2 {a} = let open ≈-Reasoning (A) in
             begin
                TMap μ a o (FMap T (TMap η a ))
             ≈⟨⟩
                (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
             ≈⟨ sym (distr U ) ⟩
                FMap U ( B [  (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])
             ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
                FMap U ( id1 B (FObj F a) )
             ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩
                id (FObj T a)
             ∎