# HG changeset patch # User Shinji KONO # Date 1488612417 -32400 # Node ID d3cd28a71b3f1c3ecb15f02652bae4340d81477f # Parent 037af9cf038c990f7521d92b9963c3d51624de8d clean up diff -r 037af9cf038c -r d3cd28a71b3f comparison-em.agda --- 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 diff -r 037af9cf038c -r d3cd28a71b3f comparison-functor-conv.agda --- 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 --- -- -- -- -- -- -- -- - -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 - ∎ - diff -r 037af9cf038c -r d3cd28a71b3f comparison-functor.agda --- 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 diff -r 037af9cf038c -r d3cd28a71b3f em-category.agda --- 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) ∎