0
|
1 module nat where
|
|
2
|
|
3 -- Monad
|
|
4 -- Category A
|
|
5 -- A = Category
|
22
|
6 -- Functor T : A → A
|
0
|
7 --T(a) = t(a)
|
|
8 --T(f) = tf(f)
|
|
9
|
2
|
10 open import Category -- https://github.com/konn/category-agda
|
0
|
11 open import Level
|
56
|
12 --open import Category.HomReasoning
|
|
13 open import HomReasoning
|
|
14 open import cat-utility
|
0
|
15
|
1
|
16 --T(g f) = T(g) T(f)
|
|
17
|
31
|
18 open Functor
|
22
|
19 Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) → {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
|
|
20 → A [ ( FMap T (A [ g o f ] )) ≈ (A [ FMap T g o FMap T f ]) ]
|
|
21 Lemma1 = \t → IsFunctor.distr ( isFunctor t )
|
0
|
22
|
|
23
|
7
|
24 open NTrans
|
1
|
25 Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A}
|
22
|
26 → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b }
|
30
|
27 → A [ A [ FMap G f o TMap μ a ] ≈ A [ TMap μ b o FMap F f ] ]
|
22
|
28 Lemma2 = \n → IsNTrans.naturality ( isNTrans n )
|
0
|
29
|
|
30 open import Category.Cat
|
|
31
|
22
|
32 -- η : 1_A → T
|
|
33 -- μ : TT → T
|
0
|
34 -- μ(a)η(T(a)) = a
|
|
35 -- μ(a)T(η(a)) = a
|
|
36 -- μ(a)(μ(T(a))) = μ(a)T(μ(a))
|
|
37
|
|
38
|
2
|
39 open Monad
|
|
40 Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
41 { T : Functor A A }
|
7
|
42 { η : NTrans A A identityFunctor T }
|
|
43 { μ : NTrans A A (T ○ T) T }
|
22
|
44 { a : Obj A } →
|
2
|
45 ( M : Monad A T η μ )
|
30
|
46 → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ]
|
22
|
47 Lemma3 = \m → IsMonad.assoc ( isMonad m )
|
2
|
48
|
|
49
|
|
50 Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
|
22
|
51 → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
|
|
52 Lemma4 = \a → IsCategory.identityL ( Category.isCategory a )
|
0
|
53
|
3
|
54 Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
55 { T : Functor A A }
|
7
|
56 { η : NTrans A A identityFunctor T }
|
|
57 { μ : NTrans A A (T ○ T) T }
|
22
|
58 { a : Obj A } →
|
3
|
59 ( M : Monad A T η μ )
|
30
|
60 → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
22
|
61 Lemma5 = \m → IsMonad.unity1 ( isMonad m )
|
3
|
62
|
|
63 Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
|
|
64 { T : Functor A A }
|
7
|
65 { η : NTrans A A identityFunctor T }
|
|
66 { μ : NTrans A A (T ○ T) T }
|
22
|
67 { a : Obj A } →
|
3
|
68 ( M : Monad A T η μ )
|
30
|
69 → A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
22
|
70 Lemma6 = \m → IsMonad.unity2 ( isMonad m )
|
3
|
71
|
|
72 -- T = M x A
|
0
|
73 -- nat of η
|
|
74 -- g ○ f = μ(c) T(g) f
|
|
75 -- η(b) ○ f = f
|
|
76 -- f ○ η(a) = f
|
22
|
77 -- h ○ (g ○ f) = (h ○ g) ○ f
|
0
|
78
|
7
|
79
|
22
|
80 lemma12 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } →
|
|
81 ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ]
|
18
|
82 lemma12 L x y =
|
|
83 let open ≈-Reasoning ( L ) in
|
|
84 begin L [ x o y ] ∎
|
11
|
85
|
4
|
86 open Kleisli
|
22
|
87 -- η(b) ○ f = f
|
|
88 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
|
56
|
89 { T : Functor A A }
|
21
|
90 ( η : NTrans A A identityFunctor T )
|
7
|
91 { μ : NTrans A A (T ○ T) T }
|
21
|
92 { a : Obj A } ( b : Obj A )
|
|
93 ( f : Hom A a ( FObj T b) )
|
22
|
94 ( m : Monad A T η μ )
|
56
|
95 { k : Kleisli A T η μ m}
|
30
|
96 → A [ join k b (TMap η b) f ≈ f ]
|
56
|
97 Lemma7 c {T} η b f m {k} =
|
21
|
98 let open ≈-Reasoning (c)
|
|
99 μ = mu ( monad k )
|
|
100 in
|
|
101 begin
|
30
|
102 join k b (TMap η b) f
|
21
|
103 ≈⟨ refl-hom ⟩
|
30
|
104 c [ TMap μ b o c [ FMap T ((TMap η b)) o f ] ]
|
21
|
105 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
|
30
|
106 c [ c [ TMap μ b o FMap T ((TMap η b)) ] o f ]
|
28
|
107 ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩
|
22
|
108 c [ id (FObj T b) o f ]
|
21
|
109 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
|
|
110 f
|
|
111 ∎
|
7
|
112
|
22
|
113 -- f ○ η(a) = f
|
|
114 Lemma8 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
|
|
115 ( T : Functor A A )
|
|
116 ( η : NTrans A A identityFunctor T )
|
7
|
117 { μ : NTrans A A (T ○ T) T }
|
22
|
118 ( a : Obj A ) ( b : Obj A )
|
|
119 ( f : Hom A a ( FObj T b) )
|
|
120 ( m : Monad A T η μ )
|
|
121 ( k : Kleisli A T η μ m)
|
30
|
122 → A [ join k b f (TMap η a) ≈ f ]
|
22
|
123 Lemma8 c T η a b f m k =
|
|
124 begin
|
30
|
125 join k b f (TMap η a)
|
22
|
126 ≈⟨ refl-hom ⟩
|
30
|
127 c [ TMap μ b o c [ FMap T f o (TMap η a) ] ]
|
66
|
128 ≈⟨ cdr ( nat η ) ⟩
|
30
|
129 c [ TMap μ b o c [ (TMap η ( FObj T b)) o f ] ]
|
22
|
130 ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
|
30
|
131 c [ c [ TMap μ b o (TMap η ( FObj T b)) ] o f ]
|
28
|
132 ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩
|
22
|
133 c [ id (FObj T b) o f ]
|
|
134 ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
|
|
135 f
|
|
136 ∎ where
|
|
137 open ≈-Reasoning (c)
|
|
138 μ = mu ( monad k )
|
5
|
139
|
22
|
140 -- h ○ (g ○ f) = (h ○ g) ○ f
|
23
|
141 Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
|
56
|
142 { T : Functor A A }
|
|
143 { η : NTrans A A identityFunctor T }
|
|
144 { μ : NTrans A A (T ○ T) T }
|
|
145 { a b c d : Obj A }
|
23
|
146 ( f : Hom A a ( FObj T b) )
|
|
147 ( g : Hom A b ( FObj T c) )
|
|
148 ( h : Hom A c ( FObj T d) )
|
|
149 ( m : Monad A T η μ )
|
56
|
150 { k : Kleisli A T η μ m}
|
22
|
151 → A [ join k d h (join k c g f) ≈ join k d ( join k d h g) f ]
|
56
|
152 Lemma9 A {T} {η} {μ} {a} {b} {c} {d} f g h m {k} =
|
24
|
153 begin
|
23
|
154 join k d h (join k c g f)
|
30
|
155 ≈⟨⟩
|
|
156 join k d h ( ( TMap μ c o ( FMap T g o f ) ) )
|
28
|
157 ≈⟨ refl-hom ⟩
|
30
|
158 ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) )
|
28
|
159 ≈⟨ cdr ( cdr ( assoc )) ⟩
|
30
|
160 ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) )
|
28
|
161 ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h )
|
30
|
162 ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) )
|
25
|
163 ≈⟨ assoc ⟩
|
30
|
164 ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f )
|
28
|
165 ≈⟨ car (sym assoc) ⟩
|
30
|
166 ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f )
|
28
|
167 ≈⟨ car ( cdr (assoc) ) ⟩
|
30
|
168 ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f )
|
28
|
169 ≈⟨ car assoc ⟩
|
30
|
170 ( ( ( TMap μ d o ( FMap T h o TMap μ c ) ) o FMap T g ) o f )
|
28
|
171 ≈⟨ car (car ( cdr ( begin
|
30
|
172 ( FMap T h o TMap μ c )
|
66
|
173 ≈⟨ nat μ ⟩
|
30
|
174 ( TMap μ (FObj T d) o FMap T (FMap T h) )
|
25
|
175 ∎
|
|
176 ))) ⟩
|
30
|
177 ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f )
|
28
|
178 ≈⟨ car (sym assoc) ⟩
|
30
|
179 ( ( TMap μ d o ( ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f )
|
28
|
180 ≈⟨ car ( cdr (sym assoc) ) ⟩
|
30
|
181 ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f )
|
28
|
182 ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩
|
30
|
183 ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f )
|
28
|
184 ≈⟨ car assoc ⟩
|
30
|
185 ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f )
|
28
|
186 ≈⟨ car ( car (
|
27
|
187 begin
|
30
|
188 ( TMap μ d o TMap μ (FObj T d) )
|
27
|
189 ≈⟨ IsMonad.assoc ( isMonad m) ⟩
|
30
|
190 ( TMap μ d o FMap T (TMap μ d) )
|
27
|
191 ∎
|
|
192 )) ⟩
|
30
|
193 ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f )
|
28
|
194 ≈⟨ car (sym assoc) ⟩
|
30
|
195 ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f )
|
24
|
196 ≈⟨ sym assoc ⟩
|
30
|
197 ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) )
|
28
|
198 ≈⟨ cdr ( car ( sym ( distr T ))) ⟩
|
30
|
199 ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) )
|
23
|
200 ≈⟨ refl-hom ⟩
|
30
|
201 join k d ( ( TMap μ d o ( FMap T h o g ) ) ) f
|
23
|
202 ≈⟨ refl-hom ⟩
|
|
203 join k d ( join k d h g) f
|
24
|
204 ∎ where open ≈-Reasoning (A)
|
3
|
205
|
56
|
206 -- Kleisli-join : {!!}
|
|
207 -- Kleisli-join = {!!}
|
3
|
208
|
56
|
209 -- Kleisli-id : {!!}
|
|
210 -- Kleisli-id = {!!}
|
|
211
|
|
212 -- Lemma10 : {!!}
|
|
213 -- Lemma10 = {!!}
|
|
214
|
|
215 -- open import Relation.Binary.Core
|
|
216
|
|
217 -- isKleisliCategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
|
|
218 -- { T : Functor A A }
|
|
219 -- { η : NTrans A A identityFunctor T }
|
|
220 -- { μ : NTrans A A (T ○ T) T }
|
|
221 -- ( m : Monad A T η μ )
|
63
|
222 -- { k : Kleisli A T η μ m} →
|
56
|
223 -- IsCategory ( Obj A ) ( Hom A ) ( Category._≈_ A ) ( Kleisli-join ) Kleisli-id
|
|
224 -- isKleisliCategory A {T} {η} m = record { isEquivalence = IsCategory.isEquivalence ( Category.isCategory A )
|
|
225 -- ; identityL = {!!}
|
|
226 -- ; identityR = {!!}
|
|
227 -- ; o-resp-≈ = {!!}
|
|
228 -- ; associative = {!!}
|
|
229 -- }
|
|
230 -- where
|
|
231 -- KidL : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) { T : Functor A A }
|
|
232 -- { η : NTrans A A identityFunctor T }
|
63
|
233 -- { μ : NTrans A A (T ○ T) T } ( m : Monad A T η μ ) → {!!}
|
56
|
234 -- KidL = {!!}
|
|
235 -- KidR : {!!}
|
|
236 -- KidR = {!!}
|
|
237 -- Ko-resp : {!!}
|
|
238 -- Ko-resp = {!!}
|
|
239 -- Kassoc : {!!}
|
|
240 -- Kassoc = {!!}
|
3
|
241
|
|
242 -- Kleisli :
|
|
243 -- Kleisli = record { Hom =
|
|
244 -- ; Hom = _⟶_
|
|
245 -- ; Id = IdProd
|
|
246 -- ; _o_ = _∘_
|
|
247 -- ; _≈_ = _≈_
|
|
248 -- ; isCategory = record { isEquivalence = record { refl = λ {φ} → ≈-refl {φ = φ}
|
|
249 -- ; sym = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
|
|
250 -- ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
|
|
251 -- }
|
|
252 -- ; identityL = identityL
|
|
253 -- ; identityR = identityR
|
|
254 -- ; o-resp-≈ = o-resp-≈
|
|
255 -- ; associative = associative
|
|
256 -- }
|
|
257 -- }
|
56
|
258
|
63
|
259 ----
|
|
260 --
|
|
261 -- Adjunction to Monad
|
|
262 --
|
|
263 ----
|
56
|
264
|
63
|
265 open Adjunction
|
58
|
266
|
|
267 UεF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
|
|
268 ( U : Functor B A )
|
|
269 ( F : Functor A B )
|
|
270 ( ε : NTrans B B ( F ○ U ) identityFunctor ) → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F )
|
63
|
271 UεF A B U F ε = lemma11 (
|
|
272 Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○ U} {identityFunctor} ε F) ) where
|
|
273 lemma11 : NTrans A A ( U ○ ((F ○ U) ○ F )) ( U ○ (identityFunctor ○ F) )
|
66
|
274 → NTrans A A (( U ○ F ) ○ ( U ○ F )) ( U ○ F )
|
63
|
275 lemma11 n = record { TMap = \a → TMap n a; isNTrans = record { naturality = IsNTrans.naturality ( isNTrans n ) }}
|
58
|
276
|
56
|
277 Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
|
|
278 { U : Functor B A }
|
|
279 { F : Functor A B }
|
|
280 { η : NTrans A A identityFunctor ( U ○ F ) }
|
|
281 { ε : NTrans B B ( F ○ U ) identityFunctor } →
|
58
|
282 Adjunction A B U F η ε → Monad A (U ○ F) η (UεF A B U F ε)
|
56
|
283 Adj2Monad A B {U} {F} {η} {ε} adj = record {
|
|
284 isMonad = record {
|
60
|
285 assoc = assoc1;
|
|
286 unity1 = unity1;
|
|
287 unity2 = unity2
|
56
|
288 }
|
60
|
289 } where
|
|
290 T : Functor A A
|
|
291 T = U ○ F
|
|
292 μ : NTrans A A ( T ○ T ) T
|
|
293 μ = UεF A B U F ε
|
63
|
294 lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) →
|
|
295 B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ]
|
|
296 lemma-assoc1 f = IsNTrans.naturality ( isNTrans ε )
|
60
|
297 assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ]
|
62
|
298 assoc1 {a} = let open ≈-Reasoning (A) in
|
|
299 begin
|
|
300 TMap μ a o TMap μ ( FObj T a )
|
|
301 ≈⟨⟩
|
|
302 (FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F a )))))
|
66
|
303 ≈⟨ sym (distr U) ⟩
|
62
|
304 FMap U (B [ TMap ε ( FObj F a ) o TMap ε ( FObj F ( FObj U (FObj F a ))) ] )
|
63
|
305 ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩
|
62
|
306 FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] )
|
66
|
307 ≈⟨ distr U ⟩
|
62
|
308 (FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a ))))
|
|
309 ≈⟨⟩
|
|
310 TMap μ a o FMap T (TMap μ a)
|
|
311 ∎
|
60
|
312 unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
61
|
313 unity1 {a} = let open ≈-Reasoning (A) in
|
|
314 begin
|
|
315 TMap μ a o TMap η ( FObj T a )
|
|
316 ≈⟨⟩
|
|
317 (FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F a ))
|
|
318 ≈⟨ IsAdjunction.adjoint1 ( isAdjunction adj ) ⟩
|
|
319 id (FObj U ( FObj F a ))
|
|
320 ≈⟨⟩
|
|
321 id (FObj T a)
|
|
322 ∎
|
60
|
323 unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
324 unity2 {a} = let open ≈-Reasoning (A) in
|
|
325 begin
|
|
326 TMap μ a o (FMap T (TMap η a ))
|
|
327 ≈⟨⟩
|
|
328 (FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
|
66
|
329 ≈⟨ sym (distr U ) ⟩
|
60
|
330 FMap U ( B [ (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])
|
|
331 ≈⟨ (IsFunctor.≈-cong (isFunctor U)) (IsAdjunction.adjoint2 ( isAdjunction adj )) ⟩
|
|
332 FMap U ( id1 B (FObj F a) )
|
|
333 ≈⟨ IsFunctor.identity ( isFunctor U ) ⟩
|
|
334 id (FObj T a)
|
|
335 ∎
|