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 Functor

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

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 )

--        F(f)
--   F(a) ----> F(b)
--    |          |
--    |t(a)      |t(b)    G(f)t(a) = t(b)F(f)
--    |          |
--    v          v
--   G(a) ----> G(b)
--        G(f)

record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
                 ( F G : Functor D C )
                 (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A))
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
  field
    naturality : {a b : Obj D} {f : Hom D a b} 
      → C [ C [ (  FMap G f ) o  ( Trans a ) ]  ≈ C [ (Trans b ) o  (FMap F f)  ] ]
--     how to write uniquness?
--    uniqness : {d : Obj D} 
--      →  ∃{e : Trans d} -> ∀{a : Trans d}  → C [ e  ≈ a ]


record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
  field
    Trans :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
    isNTrans : IsNTrans domain codomain F G Trans

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 Trans μ a ]  ≈ A [ Trans μ 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))

record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
                 ( T : Functor A A )
                 ( η : NTrans A A identityFunctor T )
                 ( μ : NTrans A A (T ○ T) T)
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
   field
      assoc  : {a : Obj A} -> A [ A [  Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
      unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
      unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]

record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
  field
    isMonad : IsMonad A T η μ

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 [  Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ 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 )

-- nat of η


-- g ○ f = μ(c) T(g) f

-- h ○ (g ○ f) = (h ○ g) ○ f

-- η(b) ○ f = f
-- f ○ η(a) = f