Mercurial > hg > Members > kono > Proof > category
changeset 97:2feec58bb02d
seprate comparison functor
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Jul 2013 15:54:58 +0900 |
| parents | 85425bd12835 |
| children | b0ba34a27783 |
| files | comparison-functor-conv.agda nat.agda |
| diffstat | 2 files changed, 167 insertions(+), 136 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/comparison-functor-conv.agda Mon Jul 29 15:54:58 2013 +0900 @@ -0,0 +1,166 @@ +-- -- -- -- -- -- -- -- +-- 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 + { 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 η μ } + { K' : Kleisli A T η μ M' } + {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 nat {c₁} {c₂} {ℓ} {A} { T } { η } { μ } { M' } { K' } +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/nat.agda Mon Jul 29 14:47:57 2013 +0900 +++ b/nat.agda Mon Jul 29 15:54:58 2013 +0900 @@ -580,139 +580,4 @@ μ=UεF = Lemma12 } - -module comparison-functor {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 ) } - ( K : 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 Category.Cat.[_]_~_ - - ≃-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 - - 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) ] - RMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) - RMap {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) ] - RKMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b) - RKMap {a} {b} f = KtoT a b f {_} {_} (( ≃-sym (T=UF RK)) (id1 A b)) - - RMap-cong : {a b : Obj A} {f g : KHom a b} -> A [ KMap f ≈ KMap g ] -> A [ RMap f ≈ RMap g ] - RMap-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 [ RMap f ≈ RMap 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 (RMap 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 (RMap (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 (RMap f) - ≈⟨ cdr ( fcong F_K (RMap-cong f≈g)) ⟩ - TMap ε_K (FObj F_K b) o FMap F_K (RMap 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 (RMap (g * f)) - ≈⟨⟩ - TMap ε_K (FObj F_K c) o FMap F_K (A [ TMap μ_K c o A [ FMap ( U_K ○ F_K ) (RMap g) o RMap 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 ) (RMap g) o RMap 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 ) (RMap g))) o (FMap F_K (RMap 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) (RMap g))))) o (FMap F_K (RMap 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) (RMap g)))) o (FMap F_K (RMap 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) (RMap g))) o (FMap F_K (RMap 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) (RMap g))) o (FMap F_K (RMap 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) (RMap g))) o (FMap F_K (RMap 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) (RMap g)))) o (FMap F_K (RMap 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) (RMap g))))) o (FMap F_K (RMap f))) - ≈⟨ cdr ( car ( - begin - TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (RMap g)))) - ≈⟨⟩ - TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o (FMap (F_K ○ U_K) (FMap F_K (RMap g))) - ≈⟨ sym (nat ε_K) ⟩ - ( FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b)) - ∎ - )) ⟩ - TMap ε_K (FObj F_K c) o ((( FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b))) o FMap F_K (RMap f)) - ≈⟨ cdr (sym assoc) ⟩ - TMap ε_K (FObj F_K c) o (( FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (RMap f))) - ≈⟨ assoc ⟩ - (TMap ε_K (FObj F_K c) o FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (RMap f)) - ≈⟨⟩ - kfmap g o kfmap f - ∎ - +-- end