-- -- -- -- -- -- -- -- 
--  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 IsEMObj (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
   field
       identity : A [ A [ φ  o TMap η a ] ≈ id1 A a ]
       eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ] ]
open IsEMObj

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

record IsEMHom {x y : Obj A} {φ  : Hom A (FObj T x) x } {φ'  : Hom A (FObj T y) y }
              (α : Hom A x y) 
              (a : EMObj {x} {φ}) 
              (b : EMObj {y} {φ'}) : Set ℓ where
   field
       homomorphism : A [ A [ φ'  o FMap T α ]  ≈ A [ α  o φ ] ]
open IsEMHom

record Eilenberg-Moore-Hom {x y : Obj A }
              {φ  : Hom A (FObj T x) x } 
              {φ' : Hom A (FObj T y) y } 
              {α : Hom A x y} 
              (a : EMObj {x} {φ}) 
              (b : EMObj {y} {φ'}) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
   EMap    : Hom A x y
   EMap    = α
   field
       isEMHom : IsEMHom {x} {y} {φ} {φ'} α a b 
open Eilenberg-Moore-Hom

EMHom : {x y : Obj A} {φ : Hom A (FObj T x) x } {φ' : Hom A (FObj T y) y } {α : Hom A x y }
          (a : EMObj {x} {φ} ) (b : EMObj {y} {φ'} ) -> Set (c₁ ⊔ c₂ ⊔ ℓ)
EMHom {x} {y} {φ} {φ'} {α} = \a b -> Eilenberg-Moore-Hom {x} {y} {φ} {φ'} {α} a b

Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj {x} {φ})
               -> 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 {obj a} {obj a} {phi a} {phi a} {id1 A (obj a)} a a 
EM-id {a} = record { 
     isEMHom = record { homomorphism = Lemma-EM1 {obj a} {phi a} a } } 

open import Relation.Binary.Core

Lemma-EM2 : {x y z : Obj A}
            {φ   : Hom A  (FObj T x) x}
            {φ'  : Hom A  (FObj T y) y}
            {φ'' : Hom A  (FObj T z) z}
            {α  : Hom A x y}
            {α' : Hom A y z}
            (a : EMObj {x} {φ}   ) 
            (b : EMObj {y} {φ'}  ) 
            (c : EMObj {z} {φ''} ) 
            (g : EMHom {y} {z} {φ'} {φ''} {α'} b c )
            (f : EMHom {x} {y} {φ} {φ'} {α} a b)
                 -> A [ A [ φ''  o FMap T (A [ (EMap g)  o  (EMap f) ] ) ]  
                      ≈ A [ (A [ (EMap g)  o  (EMap f) ])  o φ ] ]
Lemma-EM2 {_} {_} {_} {φ} {φ'} {φ''} _ _ _ g f = let 
      open ≈-Reasoning (A) in
   begin
        φ''  o FMap T ((EMap g)  o  (EMap f))
   ≈⟨ cdr (distr T) ⟩
        φ''  o ( FMap T (EMap g)  o  FMap T (EMap f) )
   ≈⟨ assoc ⟩
        ( φ''  o FMap T (EMap g))  o  FMap T (EMap f) 
   ≈⟨ car (IsEMHom.homomorphism (isEMHom g)) ⟩
        ( EMap g o φ') o  FMap T (EMap f) 
   ≈⟨ sym assoc ⟩
        EMap g  o (φ' o  FMap T (EMap f) )
   ≈⟨ cdr (IsEMHom.homomorphism (isEMHom f)) ⟩
        EMap g  o (EMap f  o  φ)
   ≈⟨ assoc ⟩
        ( (EMap g)  o  (EMap f) )  o φ
   ∎

_*_ : {x y z : Obj A}
            {φ   : Hom A  (FObj T x) x}
            {φ'  : Hom A  (FObj T y) y}
            {φ'' : Hom A  (FObj T z) z}
            {α  : Hom A x y}
            {α' : Hom A y z}
            {a : EMObj {x} {φ}   } 
            {b : EMObj {y} {φ'}  } 
            {c : EMObj {z} {φ''} } 
            (g : EMHom {y} {z} {φ'} {φ''} {α'} b c ) 
            (f : EMHom {x} {y} {φ} {φ'} {α} a b) ->
                (EMHom {x} {z} {φ} {φ''} {A [ α' o  α ] } a c)
_*_ {x} {y} {z} {φ} {φ'} {φ''} {α} {α'} {a} {b} {c} g f = record { isEMHom = record { homomorphism = 
     Lemma-EM2 {x} {y} {z} {φ} {φ'} {φ''} {α} {α'} a b c g f } }

_∙_ :  {a b c : EMObj } -> EMHom b c -> EMHom a b -> EMHom a c
_∙_ {a} {b} {c} g f = record { isEMHom = record { homomorphism = Lemma-EM2 a b c g f } }

_≗_ :  {x y : Obj A} {φ   : Hom A  (FObj T x) x} {φ'  : Hom A  (FObj T y) y} {α α' : Hom A x y} 
            {a : EMObj {x} {φ} } {b : EMObj {y} {φ'}}
            (f : EMHom {x} {y} {φ} {φ'} {α}  a b )
            (g : EMHom {x} {y} {φ} {φ'} {α'} a b ) -> Set ℓ 
_≗_ {_} {_} {_} {_} {α} {α'} f g = A [ α ≈ α' ]


isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_  EM-id 
isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
                    ; identityL =   EMidL
                    ; identityR =   EMidR
                    ; o-resp-≈ =    EMo-resp
                    ; associative = EMassoc
                    }
     where
         open ≈-Reasoning (A) 
         isEquivalence : {x y : Obj A} {φ   : Hom A  (FObj T x) x} {φ'  : Hom A  (FObj T y) y} {α α' : Hom A x y} 
            {a : EMObj {x} {φ} } {b : EMObj {y} {φ'}} ->
               IsEquivalence {_} {_} {EMHom {x} {y} {φ} {φ'} {α}  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
             } 
         EMidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id {D} ∙ f) ≗ f
         EMidL {a} {b} {f} =  idL 
         EMidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id {C})  ≗ f
         EMidR {_} {_} {f} =  idR
         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) )

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
-- --      nat-ε
-- --      nat-η
-- --
-- -- 
-- -- 
-- -- U_T : Functor Eilenberg-MooreCategory A
-- -- U_T = record {
-- --         FObj = FObj T
-- --           ; FMap = ufmap
-- --         ; isFunctor = record
-- --         {      ≈-cong   = ≈-cong
-- --              ; identity = identity
-- --              ; distr    = distr1
-- --         }
-- --      } where
-- --         identity : {a : EMObj} →  A [ ufmap (EM-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 : EMObj} {f g : EMHom a b} → A [ EMap f ≈ EMap g ] → A [ ufmap f ≈ ufmap g ]
-- --         ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in
-- --           begin
-- --              TMap μ (b)  o FMap T (EMap f)
-- --           ≈⟨ cdr (fcong T f≈g) ⟩
-- --              TMap μ (b)  o FMap T (EMap g)
-- --           ∎
-- --         distr1 :  {a b c : EMObj} {f : EMHom a b} {g : EMHom 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 g o ufmap f
-- --           ∎
-- -- 
-- -- 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