-- -- -- -- -- -- -- -- 
--  Monad to Eilenberg-Moore  Category
--  defines U^T and F^T as a resolution of Monad
--  checks Adjointness
-- 
--   Shinji KONO <kono@ie.u-ryukyu.ac.jp>
-- -- -- -- -- -- -- -- 

-- 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 em-category { 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 η μ } where

--
--  Hom in Eilenberg-Moore Category
--
open Functor
open NTrans

record IsAlgebra {a : Obj A} { phi : Hom A (FObj T a) a } : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
   field
       identity : A [ A [ phi  o TMap η a ] ≈ id1 A a ]
       eval     : A [ A [ phi  o TMap μ a ] ≈ A [ phi o FMap T phi ] ]

record EMObj : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
   field
       a         : Obj A
       phi       : Hom A (FObj T a) a
       isAlgebra : IsAlgebra {a} {phi}
   obj : Obj A
   obj = a
   φ : Hom A (FObj T a) a
   φ = phi
open EMObj

record Eilenberg-Moore-Hom (a : EMObj ) (b : EMObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
   field
       EMap    : Hom A (obj a) (obj b)
       homomorphism : A [ A [ (φ b)  o FMap T EMap ]  ≈ A [ EMap  o (φ a) ] ]
open Eilenberg-Moore-Hom

EMHom : (a : EMObj ) (b : EMObj ) -> Set (c₁ ⊔ c₂ ⊔ ℓ)
EMHom = \a b -> Eilenberg-Moore-Hom a b

Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj )
               -> A [ A [ φ  o FMap T (id1 A x) ]  ≈ A [ (id1 A x) o φ ] ]
Lemma-EM1 {x} {φ} a = let open ≈-Reasoning (A) in
   begin
       φ o FMap T (id1 A x)
   ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩
       φ o (id1 A (FObj T x))
   ≈⟨ idR ⟩
       φ 
   ≈⟨ sym idL ⟩
       (id1 A x)  o φ
   ∎

EM-id : { a : EMObj } -> EMHom a a
EM-id {a} = record { EMap = id1 A (obj a);
     homomorphism = Lemma-EM1 {obj a} {phi a} a } 

open import Relation.Binary.Core

Lemma-EM2 : (a : EMObj ) 
            (b : EMObj ) 
            (c : EMObj ) 
            (g : EMHom b c)
            (f : EMHom a b)
                 -> A [ A [ φ c  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
                      ≈ A [ (A [ (EMap g)  o  (EMap f) ])  o φ a ] ]
Lemma-EM2 a b c g f = let 
      open ≈-Reasoning (A) in
   begin
        φ c  o FMap T ((EMap g)  o  (EMap f))
   ≈⟨ cdr (distr T) ⟩
        φ c o ( FMap T (EMap g)  o  FMap T (EMap f) )
   ≈⟨ assoc ⟩
        ( φ c o FMap T (EMap g))  o  FMap T (EMap f) 
   ≈⟨ car (homomorphism (g)) ⟩
        ( EMap g o φ b) o  FMap T (EMap f) 
   ≈⟨ sym assoc ⟩
        EMap g  o (φ b o  FMap T (EMap f) )
   ≈⟨ cdr (homomorphism (f)) ⟩
        EMap g  o (EMap f  o  φ a)
   ≈⟨ assoc ⟩
        ( (EMap g)  o  (EMap f) )  o φ a
   ∎

_∙_ :  {a b c : EMObj } -> EMHom b c -> EMHom a b -> EMHom a c
_∙_ {a} {b} {c} g f = record { EMap = A [ EMap g  o EMap f ] ; homomorphism = Lemma-EM2 a b c g f } 

_≗_ : {a : EMObj } {b : EMObj } (f g : EMHom a b ) -> Set ℓ 
_≗_ f g = A [ EMap f ≈ EMap g ]

--
-- cannot use as identityL = EMidL
--
EMidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id  ∙ f) ≗ f
EMidL {C} {D} {f} = let open ≈-Reasoning (A) in idL {obj D} 
EMidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id)  ≗ f
EMidR {C} {_} {_} = let open ≈-Reasoning (A) in  idR {obj C}
EMo-resp :  {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
                          f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g)
EMo-resp {a} {b} {c} {f} {g} {h} {i} = ( IsCategory.o-resp-≈ (Category.isCategory A) )
EMassoc :   {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
                          (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h)
EMassoc {_} {_} {_} {_} {f} {g} {h} =   ( IsCategory.associative (Category.isCategory A) )

isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_  EM-id 
isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
                    ; identityL =   IsCategory.identityL (Category.isCategory A)
                    ; identityR =   IsCategory.identityR (Category.isCategory A)
                    ; o-resp-≈ =    IsCategory.o-resp-≈ (Category.isCategory A)
                    ; associative = IsCategory.associative (Category.isCategory A)
                    }
     where
         open ≈-Reasoning (A) 
         isEquivalence : {a : EMObj } {b : EMObj } ->
               IsEquivalence {_} {_} {EMHom a b } _≗_
         isEquivalence {C} {D} =      -- this is the same function as A's equivalence but has different types
           record { refl  = refl-hom
             ; sym   = sym
             ; trans = trans-hom
             } 
Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
Eilenberg-MooreCategory =
  record { Obj = EMObj
         ; Hom = EMHom
         ; _o_ = _∙_ 
         ; _≈_ = _≗_
         ; Id  =  EM-id 
         ; isCategory = isEilenberg-MooreCategory
          }


-- Resolution
--   T = U^T U^F
--     ε^t
--     η^T

U^T : Functor Eilenberg-MooreCategory A
U^T = record {
            FObj = \a -> obj a
          ; FMap = \f -> EMap f
        ; isFunctor = record
        {      ≈-cong   = \eq -> eq
             ; identity = refl-hom
             ; distr    = refl-hom
        }
     } where open ≈-Reasoning (A) 

Lemma-EM4 : (a : Obj A ) (phi : Hom A (FObj T a) a) -> A [ A [ phi  o TMap η a ] ≈ id1 A a ]
Lemma-EM4 = ?

Lemma-EM5 : (a : Obj A ) (phi : Hom A (FObj T a) a) -> A [ A [ phi  o TMap μ a ] ≈ A [ phi o FMap T phi ] ]
Lemma-EM5 = ?

ftobj : Obj A -> EMObj
ftobj = \x -> record { a = FObj T x ; phi = TMap μ x; 
 isAlgebra = record {
      identity = Lemma-EM4 (FObj T x) ( TMap μ x);
      eval     = Lemma-EM5 (FObj T x) ( TMap μ x)
 } }

Lemma-EM6 :  (a b : EMObj ) -> (f : Hom A (obj a) (obj b))  -> 
      A [ A [ (φ b)  o FMap T f ]  ≈ A [ f  o (φ a) ] ]
Lemma-EM6 = ?

ftmap : {a b : Obj A} -> (Hom A a b) -> EMHom (ftobj a) (ftobj b)
ftmap {a} {b} f = record { EMap = FMap T f; homomorphism =  Lemma-EM6 (ftobj a) (ftobj b) (FMap T f) }

F^T : Functor A Eilenberg-MooreCategory
F^T = record {
        FObj = ftobj
        ; FMap = ftmap
        ; isFunctor = record {
               ≈-cong   = ≈-cong   
             ; identity = identity 
             ; distr    = distr 
        }
     } where 
        ≈-cong   : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → (ftmap f) ≗ (ftmap g)
        ≈-cong   = ?
        identity :  {a : Obj A} →  ftmap (id1 A a) ≗ EM-id {ftobj a}
        identity = ?
        distr    :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → ftmap (A [ g o f ]) ≗ ( ftmap g ∙ ftmap f )
        distr    = ?

--open MResolution
--
--Resolution_T : MResolution A Eilenberg-MooreCategory T U_T F_T {nat-η} {nat-ε} {nat-μ} Adj_T 
--Resolution_T = record {
--      T=UF   = Lemma11;
--      μ=UεF  = Lemma12 
--  }

-- -- end