Mercurial > hg > Members > kono > Proof > category

changeset 100:59dec035602c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Eilenberg-Moore Category start
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 30 Jul 2013 17:58:20 +0900
parents bd542a1caf08
children 0f7086b6a1a6
files em-category.agda
diffstat 1 files changed, 184 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/em-category.agda	Tue Jul 30 17:58:20 2013 +0900
@@ -0,0 +1,184 @@
+-- -- -- -- -- -- -- -- 
+--  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
+--
+
+record IsEMAlgebra { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
+     (a : Obj A)  (φ  : FObj T a -> a ) : Set c₁
+  field
+     identity : A [ A [ φ  o TMap η a ] ≈ id1 A a ]
+     eval     : A [ A [ φ  o TMap μ a ] ≈ A [ φ o FMap T φ ]
+open IsEMAlgebra
+
+record EMAlgebra { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
+     (a : Obj A)  (φ  : FObj T a -> a ) : Set  c₂
+  field
+     isEMAlbgebra : IsEMAlgebra {c₁} {c₂} {ℓ} {A} {T} a φ 
+open EMAlgebra
+     
+data EMObj { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A }
+     {a : Obj A}  {φ  : FObj T a -> a } {EMAlgebra a φ} : Set ( c₁ ⊔ c₂ )
+            emObj : (IsEMAlgebra a φ) -> EMObj {_} {_} {_} {_} {_} {a} {φ}
+
+record IsEMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
+              (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ  ) 
+              (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y φ' ) : Set c₂ where
+   field
+       homomorphism : A [ φ'  o FMap T α ]  ≈ A [ α  o φ ] ]
+open IsEMHom
+
+record EMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } 
+              (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x) 
+              (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y) : Set c₂ where
+   field
+       EMap :  Hom A x y
+       isEMHom : IsEMHom {c₁} {c₂} {ℓ} {A} {T} a b
+open EMHom
+
+EM-id : {x : Obj A} a : EMObj  EMObj {_} {_} {_} {_} {_} {a}) -> EMHom a a 
+EM-id {x = x} _ = record { EMap = id1 A x ; isEMHom = Lemma-EM1 x }
+
+open import Relation.Binary.Core
+
+_≗_ : { a : EMObj } { b : EMObj } (f g  : EMHom a b ) -> Set ℓ 
+_≗_ {a} {b} f g = A [ EMap f ≈ EMap g ]
+
+_∙_ : { a b : EMObj A } → { c : EMObj A } →
+                      ( EMHom b c) → (  EMHom a b) → EMHom a c 
+_∙_ {a} {b} {c} g f = record { EMap = A [ (EMap g)  o  (EMap f) ; isEMHom = Lemma-EM2 a b c g f }
+
+isEilenberg-MooreCategory : IsCategory ( Obj A ) EMHom _⋍_ _*_ EM-id 
+isEilenberg-MooreCategory  = record  { isEquivalence =  isEquivalence 
+                    ; identityL =   KidL
+                    ; identityR =   KidR
+                    ; o-resp-≈ =    Ko-resp
+                    ; associative = Kassoc
+                    }
+     where
+         open ≈-Reasoning (A) 
+         isEquivalence :  { a b : Obj A } ->
+               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
+             } 
+         KidL : {C D : Obj A} -> {f : EMHom C D} → (EM-id * f) ⋍ f
+         KidL {_} {_} {f} =  Lemma7 (EMap f) 
+         KidR : {C D : Obj A} -> {f : EMHom C D} → (f * EM-id) ⋍ f
+         KidR {_} {_} {f} =  Lemma8 (EMap f) 
+         Ko-resp :  {a b c : Obj A} -> {f g : EMHom a b } → {h i : EMHom  b c } → 
+                          f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
+         Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = Lemma10 {a} {b} {c} (EMap f) (EMap g) (EMap h) (EMap i) eq-fg eq-hi
+         Kassoc :   {a b c d : Obj A} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } →
+                          (f * (g * h)) ⋍ ((f * g) * h)
+         Kassoc {_} {_} {_} {_} {f} {g} {h} =  Lemma9 (EMap f) (EMap g) (EMap h) 
+
+Eilenberg-MooreCategory : Category c₁ c₂ ℓ
+Eilenberg-MooreCategory =
+  record { Obj = Obj A
+         ; 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 : Obj A} →  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 : Obj A} {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 : Obj A} {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 {a} {c} ( record { EMap = TMap μ (c) o (FMap T (EMap g)  o (EMap f)) } )
+--           ≈⟨⟩
+--              TMap μ (c)  o  FMap T ( TMap μ (c) o (FMap T (EMap g)  o (EMap f)))
+--           ≈⟨ cdr ( distr T) ⟩
+--              TMap μ (c)  o (( FMap T ( TMap μ (c)) o FMap T  (FMap T (EMap g)  o (EMap f))))
+--           ≈⟨ assoc ⟩
+--              (TMap μ (c)  o ( FMap T ( TMap μ (c)))) o FMap T  (FMap T (EMap g)  o (EMap f))
+--           ≈⟨ car (sym (IsMonad.assoc (isMonad M))) ⟩
+--              (TMap μ (c)  o ( TMap μ (FObj T c))) o FMap T  (FMap T (EMap g)  o (EMap f))
+--           ≈⟨ sym assoc ⟩
+--              TMap μ (c)  o (( TMap μ (FObj T c)) o FMap T  (FMap T (EMap g)  o (EMap f)))
+--           ≈⟨ cdr (cdr (distr T)) ⟩
+--              TMap μ (c)  o (( TMap μ (FObj T c)) o (FMap T  (FMap T (EMap g))  o FMap T (EMap f)))
+--           ≈⟨ cdr (assoc) ⟩
+--              TMap μ (c)  o ((( TMap μ (FObj T c)) o (FMap T  (FMap T (EMap g))))  o FMap T (EMap f))
+--           ≈⟨ sym (cdr (car (nat μ ))) ⟩
+--              TMap μ (c)  o ((FMap T (EMap g )  o  TMap μ (b))  o FMap T (EMap f ))
+--           ≈⟨ cdr (sym assoc) ⟩
+--              TMap μ (c)  o (FMap T (EMap g )  o  ( TMap μ (b)  o FMap T (EMap f )))
+--           ≈⟨ assoc ⟩
+--              ( TMap μ (c)  o FMap T (EMap g ) )  o  ( TMap μ (b)  o FMap T (EMap 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