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