Mercurial > hg > Members > kono > Proof > category

changeset 465:d3cd28a71b3f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Mar 2017 16:26:57 +0900
parents 037af9cf038c
children 44bd77c80555
files comparison-em.agda comparison-functor-conv.agda comparison-functor.agda em-category.agda
diffstat 4 files changed, 12 insertions(+), 184 deletions(-) [+]
line wrap: on
line diff
--- a/comparison-em.agda	Sat Mar 04 11:05:55 2017 +0900
+++ b/comparison-em.agda	Sat Mar 04 16:26:57 2017 +0900
@@ -27,7 +27,7 @@
       { μ^K : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) }
       ( Adj^K : Adjunction A B U^K F^K η^K ε^K )
       ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K} Adj^K )
-where
+  where
 
 open import adj-monad
 
@@ -45,11 +45,11 @@
 open NTrans
 open Adjunction
 open MResolution
-open Eilenberg-Moore-Hom
+open EMHom
 
 emkobj : Obj B → EMObj
 emkobj b = record { 
-     a = FObj U^K b ; phi = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1 b; eval = eval1 b }
+     obj = FObj U^K b ; φ = FMap U^K (TMap ε^K b) ; isAlgebra = record { identity = identity1 b; eval = eval1 b }
   } where
       identity1 :  (b : Obj B) → A [ A [ (FMap U^K (TMap ε^K b))  o TMap η^K (FObj U^K b) ] ≈ id1 A (FObj U^K b) ]
       identity1 b =  let open ≈-Reasoning (A) in
--- a/comparison-functor-conv.agda	Sat Mar 04 11:05:55 2017 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,165 +0,0 @@
--- -- -- -- -- -- -- -- 
---  Comparison Functor of Kelisli Category
---  defines U_K and F_K as a resolution of Monad
---  checks Adjointness
--- 
---   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 import cat-utility
-open import Category.Cat
-open import Relation.Binary.Core
-
-
-module comparison-functor-conv
-      { 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 η μ }
-      {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) 
-      { U_K : Functor B A } { F_K : Functor A B }
-      { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
-      { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } 
-      { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } 
-      ( M :  Monad A (U_K ○ F_K) η_K μ_K )
-      ( AdjK : Adjunction A B U_K F_K η_K ε_K )
-      ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K} AdjK )
-  where
-
-open import kleisli {c₁} {c₂} {ℓ} {A} { T } { η } { μ } { M' } 
-open Functor
-open NTrans
-open Category.Cat.[_]_~_
-open MResolution
-
-≃-sym : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' } 
-      {F G : Functor C D} → F ≃ G → G ≃ F
-≃-sym {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f)
-  where
-    helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] g ~ f
-    helper (Category.Cat.refl Ff≈Gf) = 
-                   Category.Cat.refl {C = D} (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory D)) Ff≈Gf)
-
--- to T=UF constraints happy 
-hoge : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' } 
-      {F G : Functor C D} → F ≃ G → F ≃ G
-hoge {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f)
-  where
-    helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] f ~ g
-    helper (Category.Cat.refl Ff≈Gf) = Category.Cat.refl Ff≈Gf
-
-open KleisliHom
-
-RHom  = λ (a b : Obj A) → KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b
-TtoK : (a b : Obj A) → (KHom a b) →  {g h : Hom A  (FObj T b) (FObj ( U_K ○ F_K) b) } →
-      ([ A ] g ~ h) → Hom A a (FObj ( U_K ○ F_K ) b)  
-TtoK  _ _ f {g} (Category.Cat.refl _) = A [ g o (KMap f) ]
-TKMap : {a b : Obj A} → (f : KHom a b) → Hom A a (FObj ( U_K ○ F_K ) b) 
-TKMap  {a} {b} f = TtoK a b f {_} {_} ((hoge (T=UF RK)) (id1 A b)) 
-
-KtoT : (a b : Obj A) → (RHom a b) → {g h : Hom A  (FObj ( U_K ○ F_K ) b) (FObj  T b) } →
-      ([ A ] g ~ h) → Hom A a (FObj T b)  
-KtoT  _ _ f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ]
-KTMap : {a b : Obj A} → (f : RHom a b) → Hom A a (FObj T b) 
-KTMap {a} {b} f = KtoT a b f {_} {_}  (( ≃-sym (T=UF RK)) (id1 A b))
-
-TKMap-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ TKMap f ≈ TKMap g ]
-TKMap-cong {a} {b} {f} {g} eq = helper a b f g eq ((hoge (T=UF RK))( id1 A b  )) 
-  where 
-        open ≈-Reasoning (A)
-        helper : (a b : Obj A) (f g : KHom a b) → A [ KMap f ≈ KMap g ] →
-                 {conv : Hom A  (FObj T b) (FObj ( U_K ○ F_K ) b) } → ([ A ] conv ~ conv) → A [ TKMap f ≈ TKMap g ]
-        helper _ _ _ _ eq (Category.Cat.refl _) = 
-            (Category.IsCategory.o-resp-≈ (Category.isCategory A)) eq refl-hom
-
-kfmap : {a b : Obj A} (f : KHom a b) → Hom B (FObj F_K a) (FObj F_K b)
-kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (TKMap f) ]
-
-open Adjunction
-K_T : Functor KleisliCategory B 
-K_T = record {
-          FObj = FObj F_K
-        ; FMap = kfmap
-        ; isFunctor = record
-        {      ≈-cong   = ≈-cong
-             ; identity = identity
-             ; distr    = distr1
-        }
-     } where
-         identity : {a : Obj A} →  B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ]
-         identity {a} = let open ≈-Reasoning (B) in
-           begin
-               kfmap (K-id {a})
-           ≈⟨⟩
-               TMap ε_K (FObj F_K a) o FMap F_K (TKMap (K-id {a}))
-           ≈⟨⟩
-              TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a)
-           ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
-              id1 B (FObj F_K a)
-           ∎
-         ≈-cong : {a b : Obj A} → {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
-         ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
-           begin
-               kfmap f
-           ≈⟨⟩
-               TMap ε_K (FObj F_K b) o FMap F_K (TKMap f)
-           ≈⟨ cdr ( fcong F_K (TKMap-cong f≈g))  ⟩
-               TMap ε_K (FObj F_K b) o FMap F_K (TKMap g)
-           ≈⟨⟩
-               kfmap g
-           ∎
-         distr1 :  {a b c : Obj A} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )]
-         distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
-           begin
-              kfmap (g * f)
-           ≈⟨⟩
-              TMap ε_K (FObj F_K c) o FMap F_K (TKMap (g * f))
-           ≈⟨⟩
-              TMap ε_K (FObj F_K c) o FMap F_K (A [ TMap μ_K c o A [ FMap ( U_K ○ F_K ) (TKMap g)  o TKMap f ] ] )
-           ≈⟨ cdr ( distr F_K ) ⟩
-              TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o ( FMap F_K (A  [ FMap ( U_K ○ F_K ) (TKMap g)  o TKMap f ])))
-           ≈⟨ cdr (cdr ( distr F_K )) ⟩
-              TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o (( FMap F_K (FMap ( U_K ○ F_K ) (TKMap g))) o (FMap F_K (TKMap f))))
-           ≈⟨ cdr assoc ⟩
-              TMap ε_K (FObj F_K c) o ((( FMap F_K (TMap μ_K c) o ( FMap F_K (FMap (U_K ○ F_K) (TKMap g))))) o (FMap F_K (TKMap f)))
-           ≈⟨ cdr (car (car ( fcong F_K ( μ=UεF RK )))) ⟩
-              TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )) o 
-                                  ( FMap F_K (FMap (U_K ○ F_K) (TKMap g)))) o (FMap F_K (TKMap f)))
-           ≈⟨ sym (cdr assoc)  ⟩
-              TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) ))) o 
-                                  (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))) o (FMap F_K (TKMap f))))
-           ≈⟨ assoc ⟩
-              (TMap ε_K (FObj F_K c) o ( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )))) o 
-                                  (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))) o (FMap F_K (TKMap f)))
-           ≈⟨ car (sym (nat ε_K)) ⟩
-              (TMap ε_K (FObj F_K c) o ( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)))) o 
-                                  (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))) o (FMap F_K (TKMap f)))
-           ≈⟨ sym assoc ⟩
-              TMap ε_K (FObj F_K c) o (( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o 
-                                  ((( FMap F_K (FMap (U_K ○ F_K) (TKMap g)))) o (FMap F_K (TKMap f))))
-           ≈⟨ cdr assoc ⟩
-              TMap ε_K (FObj F_K c) o ((( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o 
-                                  (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))))) o (FMap F_K (TKMap f)))
-           ≈⟨ cdr ( car (
-               begin
-                    TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (TKMap g))))
-                 ≈⟨⟩
-                    TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o  (FMap (F_K ○ U_K) (FMap F_K (TKMap g))) 
-                 ≈⟨ sym (nat ε_K)  ⟩
-                    ( FMap F_K (TKMap g)) o (TMap ε_K (FObj F_K b))
-               ∎
-           ))  ⟩
-              TMap ε_K (FObj F_K c) o ((( FMap F_K (TKMap g)) o (TMap ε_K (FObj F_K b))) o FMap F_K (TKMap f))
-           ≈⟨ cdr (sym assoc) ⟩
-              TMap ε_K (FObj F_K c) o (( FMap F_K (TKMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (TKMap f)))
-           ≈⟨ assoc ⟩
-              (TMap ε_K (FObj F_K c) o FMap F_K (TKMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (TKMap f))
-           ≈⟨⟩
-              kfmap g o kfmap f
-           ∎
-
--- a/comparison-functor.agda	Sat Mar 04 11:05:55 2017 +0900
+++ b/comparison-functor.agda	Sat Mar 04 16:26:57 2017 +0900
@@ -27,7 +27,7 @@
       { μ_K' : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) }
       ( AdjK : Adjunction A B U_K F_K η_K ε_K )
       ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K'} AdjK )
-where
+   where
 
 open import adj-monad
 
--- a/em-category.agda	Sat Mar 04 11:05:55 2017 +0900
+++ b/em-category.agda	Sat Mar 04 16:26:57 2017 +0900
@@ -39,23 +39,16 @@
 
 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
+       obj     : Obj A
+       φ       : Hom A (FObj T obj) obj
+       isAlgebra : IsAlgebra {obj} {φ}
 open EMObj
 
-record Eilenberg-Moore-Hom (a : EMObj ) (b : EMObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
+record EMHom (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
+open EMHom
 
 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 φ ] ]
@@ -72,7 +65,7 @@
 
 EM-id : { a : EMObj } → EMHom a a
 EM-id {a} = record { EMap = id1 A (obj a);
-     homomorphism = Lemma-EM1 {obj a} {phi a} a } 
+     homomorphism = Lemma-EM1 {obj a} {φ a} a } 
 
 open import Relation.Binary.Core
 
@@ -182,7 +175,7 @@
     ∎
 
 ftobj : Obj A → EMObj
-ftobj = λ x → record { a = FObj T x ; phi = TMap μ x; 
+ftobj = λ x → record { obj = FObj T x ; φ = TMap μ x; 
  isAlgebra = record {
       identity = Lemma-EM4 x;
       eval     = Lemma-EM5 x
@@ -340,7 +333,7 @@
                ≈⟨⟩ 
                    φ b  o TMap η (obj b)
                ≈⟨ IsAlgebra.identity (isAlgebra b) ⟩
-                   id1 A (a b)
+                   id1 A (obj b)
                ≈⟨⟩ 
                    id1 A (FObj U^T b)
                ∎