module cat-utility where

-- Shinji KONO <kono@ie.u-ryukyu.ac.jp>

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

open Functor

id1 :   ∀{c₁ c₂ ℓ  : Level} (A : Category c₁ c₂ ℓ)  (a  : Obj A ) →  Hom A a a
id1 A a =  (Id {_} {_} {_} {A} a)

record IsUniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                 ( U : Functor B A )
                 ( F : Obj A → Obj B )
                 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
                 ( _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
   field
       universalMapping :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → 
                     A [ A [ FMap U ( f * ) o  η a' ]  ≈ f ]
       uniquness :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g :  Hom B (F a') b' } → 
                     A [ A [ FMap U g o  η a' ]  ≈ f ] → B [ f * ≈ g ]

record UniversalMapping  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') 
                 ( U : Functor B A )
                 ( F : Obj A → Obj B )
                 ( η : (a : Obj A) → Hom A a ( FObj U (F a) ) )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
    infixr 11 _*
    field
       _* :  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b 
       isUniversalMapping : IsUniversalMapping A B U F η _*

open NTrans
open import Category.Cat
record IsAdjunction  {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 )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
   field
       adjoint1 :   { b : Obj B } →
                     A [ A [ ( FMap U ( TMap ε b ))  o ( TMap η ( FObj U b )) ]  ≈ id1 A (FObj U b) ]
       adjoint2 :   {a : Obj A} →
                     B [ B [ ( TMap ε ( FObj F a ))  o ( FMap F ( TMap η a )) ]  ≈ id1 B (FObj F a) ]

record Adjunction {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 )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
    field
       isAdjunction : IsAdjunction A B U F η ε


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 [ TMap μ a o TMap μ ( FObj T a ) ] ≈  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) ]
      unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η 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
  eta : NTrans A A identityFunctor T
  eta = η
  mu : NTrans A A (T ○ T) T
  mu = μ
  field
    isMonad : IsMonad A T η μ

Functor*Nat :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
    (F : Functor B C) -> { G H : Functor A B } -> ( n : NTrans A B G H ) -> NTrans A C (F ○  G) (F ○ H)
Functor*Nat A {B} C F {G} {H} n = record {
       TMap  = \a -> FMap F (TMap n a)
       ; isNTrans = record {
            naturality = naturality
       }
    } where
         naturality : {a b : Obj A} {f : Hom A a b} 
            → C [ C [ (FMap F ( FMap H f )) o  ( FMap F (TMap n a)) ]  ≈ C [ (FMap F (TMap n b )) o  (FMap F (FMap G f))  ] ]
         naturality  {a} {b} {f}  = let open ≈-Reasoning (C) in
            begin  
               (FMap F ( FMap H f )) o  ( FMap F (TMap n a))
            ≈⟨ sym (distr F) ⟩
               FMap F ( B [ (FMap H f)  o TMap n a ])
            ≈⟨ IsFunctor.≈-cong (isFunctor F) ( nat n ) ⟩
               FMap F ( B [ (TMap n b ) o FMap G f ] )
            ≈⟨ distr F ⟩
               (FMap F (TMap n b )) o  (FMap F (FMap G f))
            ∎

Nat*Functor :  {c₁ c₂ ℓ c₁' c₂' ℓ' c₁'' c₂'' ℓ'' : Level} (A : Category c₁ c₂ ℓ) {B : Category c₁' c₂' ℓ'} (C : Category c₁'' c₂'' ℓ'')
    { G H : Functor B C } -> ( n : NTrans B C G H ) -> (F : Functor A B) -> NTrans A C (G ○  F) (H ○ F)
Nat*Functor A {B} C {G} {H} n F = record {
       TMap  = \a -> TMap n (FObj F a)
       ; isNTrans = record {
            naturality = naturality
       }
    } where
         naturality : {a b : Obj A} {f : Hom A a b} 
            → C [ C [ ( FMap H (FMap F f )) o  ( TMap n (FObj F a)) ]  ≈ C [ (TMap n (FObj F b )) o  (FMap G (FMap F f))  ] ]
         naturality  {a} {b} {f}  =  IsNTrans.naturality ( isNTrans n) 

record Kleisli  { 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 η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
     monad : Monad A T η μ 
     monad = M
     -- g ○ f = μ(c) T(g) f
     join : { a b : Obj A } → { c : Obj A } →
                      ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
     join {_} {_} {c} g f = A [ TMap μ c  o A [ FMap T g o f ] ]