Mercurial > hg > Members > kono > Proof > category

comparison comparison-functor-conv.agda @ 97:2feec58bb02d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
seprate comparison functor
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jul 2013 15:54:58 +0900
parents
children b0ba34a27783
comparison
equal deleted inserted replaced
96:85425bd12835 97:2feec58bb02d
1 -- -- -- -- -- -- -- --
2 -- Comparison Functor of Kelisli Category
3 -- defines U_K and F_K as a resolution of Monad
4 -- checks Adjointness
5 --
6 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
7 -- -- -- -- -- -- -- --
8
9 open import Category -- https://github.com/konn/category-agda
10 open import Level
11 --open import Category.HomReasoning
12 open import HomReasoning
13 open import cat-utility
14 open import Category.Cat
15 open import Relation.Binary.Core
16
17
18 module comparison-functor
19 { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
20 { T : Functor A A }
21 { η : NTrans A A identityFunctor T }
22 { μ : NTrans A A (T ○ T) T }
23 { M' : Monad A T η μ }
24 { K' : Kleisli A T η μ M' }
25 {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' )
26 { U_K : Functor B A } { F_K : Functor A B }
27 { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) }
28 { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor }
29 { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) }
30 ( M : Monad A (U_K ○ F_K) η_K μ_K )
31 ( AdjK : Adjunction A B U_K F_K η_K ε_K )
32 ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K} AdjK )
33 where
34
35 open import nat {c₁} {c₂} {ℓ} {A} { T } { η } { μ } { M' } { K' }
36 open Functor
37 open NTrans
38 open Category.Cat.[_]_~_
39 open MResolution
40
41 ≃-sym : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' }
42 {F G : Functor C D} → F ≃ G → G ≃ F
43 ≃-sym {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f)
44 where
45 helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] g ~ f
46 helper (Category.Cat.refl Ff≈Gf) =
47 Category.Cat.refl {C = D} (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory D)) Ff≈Gf)
48
49 -- to T=UF constraints happy
50 hoge : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' }
51 {F G : Functor C D} → F ≃ G → F ≃ G
52 hoge {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f)
53 where
54 helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] f ~ g
55 helper (Category.Cat.refl Ff≈Gf) = Category.Cat.refl Ff≈Gf
56
57 open KleisliHom
58
59 RHom = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b
60 TtoK : (a b : Obj A) -> (KHom a b) -> {g h : Hom A (FObj T b) (FObj ( U_K ○ F_K) b) } ->
61 ([ A ] g ~ h) -> Hom A a (FObj ( U_K ○ F_K ) b)
62 TtoK _ _ f {g} (Category.Cat.refl _) = A [ g o (KMap f) ]
63 TKMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b)
64 TKMap {a} {b} f = TtoK a b f {_} {_} ((hoge (T=UF RK)) (id1 A b))
65
66 KtoT : (a b : Obj A) -> (RHom a b) -> {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } ->
67 ([ A ] g ~ h) -> Hom A a (FObj T b)
68 KtoT _ _ f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ]
69 KTMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b)
70 KTMap {a} {b} f = KtoT a b f {_} {_} (( ≃-sym (T=UF RK)) (id1 A b))
71
72 TKMap-cong : {a b : Obj A} {f g : KHom a b} -> A [ KMap f ≈ KMap g ] -> A [ TKMap f ≈ TKMap g ]
73 TKMap-cong {a} {b} {f} {g} eq = helper a b f g eq ((hoge (T=UF RK))( id1 A b ))
74 where
75 open ≈-Reasoning (A)
76 helper : (a b : Obj A) (f g : KHom a b) -> A [ KMap f ≈ KMap g ] ->
77 {conv : Hom A (FObj T b) (FObj ( U_K ○ F_K ) b) } -> ([ A ] conv ~ conv) -> A [ TKMap f ≈ TKMap g ]
78 helper _ _ _ _ eq (Category.Cat.refl _) =
79 (Category.IsCategory.o-resp-≈ (Category.isCategory A)) eq refl-hom
80
81 kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b)
82 kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (TKMap f) ]
83
84 open Adjunction
85 K_T : Functor KleisliCategory B
86 K_T = record {
87 FObj = FObj F_K
88 ; FMap = kfmap
89 ; isFunctor = record
90 { ≈-cong = ≈-cong
91 ; identity = identity
92 ; distr = distr1
93 }
94 } where
95 identity : {a : Obj A} → B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ]
96 identity {a} = let open ≈-Reasoning (B) in
97 begin
98 kfmap (K-id {a})
99 ≈⟨⟩
100 TMap ε_K (FObj F_K a) o FMap F_K (TKMap (K-id {a}))
101 ≈⟨⟩
102 TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a)
103 ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩
104 id1 B (FObj F_K a)
105 ∎
106 ≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ]
107 ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in
108 begin
109 kfmap f
110 ≈⟨⟩
111 TMap ε_K (FObj F_K b) o FMap F_K (TKMap f)
112 ≈⟨ cdr ( fcong F_K (TKMap-cong f≈g)) ⟩
113 TMap ε_K (FObj F_K b) o FMap F_K (TKMap g)
114 ≈⟨⟩
115 kfmap g
116 ∎
117 distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )]
118 distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in
119 begin
120 kfmap (g * f)
121 ≈⟨⟩
122 TMap ε_K (FObj F_K c) o FMap F_K (TKMap (g * f))
123 ≈⟨⟩
124 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 ] ] )
125 ≈⟨ cdr ( distr F_K ) ⟩
126 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 ])))
127 ≈⟨ cdr (cdr ( distr F_K )) ⟩
128 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))))
129 ≈⟨ cdr assoc ⟩
130 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)))
131 ≈⟨ cdr (car (car ( fcong F_K ( μ=UεF RK )))) ⟩
132 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )) o
133 ( FMap F_K (FMap (U_K ○ F_K) (TKMap g)))) o (FMap F_K (TKMap f)))
134 ≈⟨ sym (cdr assoc) ⟩
135 TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) ))) o
136 (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))) o (FMap F_K (TKMap f))))
137 ≈⟨ assoc ⟩
138 (TMap ε_K (FObj F_K c) o ( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )))) o
139 (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))) o (FMap F_K (TKMap f)))
140 ≈⟨ car (sym (nat ε_K)) ⟩
141 (TMap ε_K (FObj F_K c) o ( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)))) o
142 (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))) o (FMap F_K (TKMap f)))
143 ≈⟨ sym assoc ⟩
144 TMap ε_K (FObj F_K c) o (( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o
145 ((( FMap F_K (FMap (U_K ○ F_K) (TKMap g)))) o (FMap F_K (TKMap f))))
146 ≈⟨ cdr assoc ⟩
147 TMap ε_K (FObj F_K c) o ((( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o
148 (( FMap F_K (FMap (U_K ○ F_K) (TKMap g))))) o (FMap F_K (TKMap f)))
149 ≈⟨ cdr ( car (
150 begin
151 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (TKMap g))))
152 ≈⟨⟩
153 TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o (FMap (F_K ○ U_K) (FMap F_K (TKMap g)))
154 ≈⟨ sym (nat ε_K) ⟩
155 ( FMap F_K (TKMap g)) o (TMap ε_K (FObj F_K b))
156 ∎
157 )) ⟩
158 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))
159 ≈⟨ cdr (sym assoc) ⟩
160 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)))
161 ≈⟨ assoc ⟩
162 (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))
163 ≈⟨⟩
164 kfmap g o kfmap f
165 ∎
166