Mercurial > hg > Members > kono > Proof > category
annotate equalizer.agda @ 225:1a9f20917fbd
comment
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 05 Sep 2013 14:56:35 +0900 |
parents | a9d311cea336 |
children | 27f2c77c963f |
rev | line source |
---|---|
205 | 1 --- |
2 -- | |
3 -- Equalizer | |
4 -- | |
208 | 5 -- e f |
205 | 6 -- c --------> a ----------> b |
208 | 7 -- ^ . ----------> |
205 | 8 -- | . g |
208 | 9 -- |k . |
10 -- | . h | |
205 | 11 -- d |
12 -- | |
13 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp> | |
14 ---- | |
15 | |
16 open import Category -- https://github.com/konn/category-agda | |
17 open import Level | |
18 module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where | |
19 | |
20 open import HomReasoning | |
21 open import cat-utility | |
22 | |
209 | 23 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where |
205 | 24 field |
209 | 25 e : Hom A c a |
221 | 26 fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] |
209 | 27 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c |
215 | 28 ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] |
29 uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → | |
214 | 30 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] |
209 | 31 equalizer : Hom A c a |
32 equalizer = e | |
206 | 33 |
225 | 34 -- |
35 -- Flat Equational Definition of Equalizer | |
36 -- | |
37 record Burroni { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where | |
206 | 38 field |
212 | 39 α : {a b c : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → Hom A c a |
214 | 40 γ : {a b c d : Obj A } → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c |
212 | 41 δ : {a b c : Obj A } → (f : Hom A a b) → Hom A a c |
213 | 42 b1 : A [ A [ f o α {a} {b} {a} f g ] ≈ A [ g o α f g ] ] |
214 | 43 b2 : {d : Obj A } → {h : Hom A d a } → A [ A [ ( α f g) o (γ {a} {b} {c} f g h) ] ≈ A [ h o α (A [ f o h ]) (A [ g o h ]) ] ] |
213 | 44 b3 : A [ A [ α f f o δ {a} {b} {a} f ] ≈ id1 A a ] |
207
22811f7a04e1
Equalizer problems have written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
206
diff
changeset
|
45 -- b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ] |
215 | 46 b4 : {d : Obj A } {k : Hom A d c} → A [ A [ γ {a} {b} {c} {d} f g ( A [ α {a} {b} {c} f g o k ] ) o δ (A [ f o A [ α f g o k ] ] ) ] ≈ k ] |
207
22811f7a04e1
Equalizer problems have written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
206
diff
changeset
|
47 -- A [ α f g o β f g h ] ≈ h |
214 | 48 β : { d e a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → Hom A d c |
49 β {d} {e} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ] | |
207
22811f7a04e1
Equalizer problems have written
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
206
diff
changeset
|
50 |
209 | 51 open Equalizer |
225 | 52 open Burroni |
209 | 53 |
225 | 54 -- |
55 -- Some obvious conditions for k (fe = ge) → ( fh = gh ) | |
56 -- | |
219 | 57 |
224 | 58 f1=g1 : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → (h : Hom A c a) → A [ A [ f o h ] ≈ A [ g o h ] ] |
59 f1=g1 eq h = let open ≈-Reasoning (A) in (resp refl-hom eq ) | |
60 | |
61 f1=gh : { a b c d : Obj A } {f g : Hom A a b } → { e : Hom A c a } → { h : Hom A d c } → | |
62 (eq : A [ A [ f o e ] ≈ A [ g o e ] ] ) → A [ A [ f o A [ e o h ] ] ≈ A [ g o A [ e o h ] ] ] | |
63 f1=gh {a} {b} {c} {d} {f} {g} {e} {h} eq = let open ≈-Reasoning (A) in | |
64 begin | |
65 f o ( e o h ) | |
66 ≈⟨ assoc ⟩ | |
67 (f o e ) o h | |
68 ≈⟨ car eq ⟩ | |
69 (g o e ) o h | |
70 ≈↑⟨ assoc ⟩ | |
71 g o ( e o h ) | |
72 ∎ | |
219 | 73 |
225 | 74 -- |
75 -- For e f f, we need e eqa = id1 A a, but it is equal to say k eqa (id a) is id | |
76 -- | |
77 -- Equalizer has free choice of c up to isomorphism, we cannot prove eqa = id a | |
219 | 78 |
79 equalizer-eq-k : { a b : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {a} f g) → | |
80 A [ e eqa ≈ id1 A a ] → | |
224 | 81 A [ k eqa (id1 A a) (f1=g1 eq (id1 A a)) ≈ id1 A a ] |
219 | 82 equalizer-eq-k {a} {b} {f} {g} eq eqa e=1 = let open ≈-Reasoning (A) in |
83 begin | |
224 | 84 k eqa (id1 A a) (f1=g1 eq (id1 A a)) |
219 | 85 ≈⟨ uniqueness eqa ( begin |
86 e eqa o id1 A a | |
87 ≈⟨ idR ⟩ | |
88 e eqa | |
89 ≈⟨ e=1 ⟩ | |
90 id1 A a | |
91 ∎ )⟩ | |
92 id1 A a | |
93 ∎ | |
94 | |
222 | 95 equalizer-eq-e : { a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {a} f g) → (eq : A [ f ≈ g ] ) → |
224 | 96 A [ k eqa (id1 A a) (f1=g1 eq (id1 A a)) ≈ id1 A a ] → |
222 | 97 A [ e eqa ≈ id1 A a ] |
98 equalizer-eq-e {a} {b} {f} {g} eqa eq k=1 = let open ≈-Reasoning (A) in | |
99 begin | |
100 e eqa | |
101 ≈↑⟨ idR ⟩ | |
102 e eqa o id1 A a | |
103 ≈↑⟨ cdr k=1 ⟩ | |
224 | 104 e eqa o k eqa (id1 A a) (f1=g1 eq (id1 A a)) |
222 | 105 ≈⟨ ek=h eqa ⟩ |
106 id1 A a | |
107 ∎ | |
108 | |
225 | 109 -- |
110 -- | |
111 -- An isomorphic element c' of c makes another equalizer | |
112 -- | |
222 | 113 -- e eqa f g f |
114 -- c ----------> a ------->b | |
115 -- |^ | |
116 -- || | |
117 -- h || h-1 | |
118 -- v| | |
119 -- c' | |
120 | |
121 equalizer+iso : {a b c c' : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) → (h-1 : Hom A c' c ) → (h : Hom A c c' ) → | |
122 A [ A [ h-1 o h ] ≈ id1 A c ] → A [ A [ h o h-1 ] ≈ id1 A c' ] | |
123 → Equalizer A {c'} f g | |
124 equalizer+iso {a} {b} {c} {c'} {f} {g} eqa h-1 h h-1-id h-id = record { | |
125 e = A [ e eqa o h-1 ] ; | |
126 fe=ge = fe=ge1 ; | |
127 k = λ j eq → A [ h o k eqa j eq ] ; | |
128 ek=h = ek=h1 ; | |
129 uniqueness = uniqueness1 | |
130 } where | |
131 fe=ge1 : A [ A [ f o A [ e eqa o h-1 ] ] ≈ A [ g o A [ e eqa o h-1 ] ] ] | |
132 fe=ge1 = let open ≈-Reasoning (A) in | |
133 begin | |
134 f o ( e eqa o h-1 ) | |
135 ≈⟨ assoc ⟩ | |
136 (f o e eqa ) o h-1 | |
137 ≈⟨ car (fe=ge eqa) ⟩ | |
138 (g o e eqa ) o h-1 | |
139 ≈↑⟨ assoc ⟩ | |
140 g o ( e eqa o h-1 ) | |
141 ∎ | |
142 ek=h1 : {d : Obj A} {j : Hom A d a} {eq : A [ A [ f o j ] ≈ A [ g o j ] ]} → | |
143 A [ A [ A [ e eqa o h-1 ] o A [ h o k eqa j eq ] ] ≈ j ] | |
144 ek=h1 {d} {j} {eq} = let open ≈-Reasoning (A) in | |
145 begin | |
146 (e eqa o h-1 ) o ( h o k eqa j eq ) | |
147 ≈↑⟨ assoc ⟩ | |
148 e eqa o ( h-1 o ( h o k eqa j eq )) | |
149 ≈⟨ cdr assoc ⟩ | |
150 e eqa o (( h-1 o h ) o k eqa j eq ) | |
151 ≈⟨ cdr (car (h-1-id )) ⟩ | |
152 e eqa o (id1 A c o k eqa j eq ) | |
153 ≈⟨ cdr idL ⟩ | |
154 e eqa o (k eqa j eq ) | |
155 ≈⟨ ek=h eqa ⟩ | |
156 j | |
157 ∎ | |
158 uniqueness1 : {d : Obj A} {h' : Hom A d a} {eq : A [ A [ f o h' ] ≈ A [ g o h' ] ]} {j : Hom A d c'} → | |
159 A [ A [ A [ e eqa o h-1 ] o j ] ≈ h' ] → | |
160 A [ A [ h o k eqa h' eq ] ≈ j ] | |
161 uniqueness1 {d} {h'} {eq} {j} ej=h = let open ≈-Reasoning (A) in | |
162 begin | |
163 h o k eqa h' eq | |
164 ≈⟨ cdr (uniqueness eqa ( | |
165 begin | |
166 e eqa o ( h-1 o j ) | |
167 ≈⟨ assoc ⟩ | |
168 (e eqa o h-1 ) o j | |
169 ≈⟨ ej=h ⟩ | |
170 h' | |
171 ∎ | |
172 )) ⟩ | |
173 h o ( h-1 o j ) | |
174 ≈⟨ assoc ⟩ | |
175 (h o h-1 ) o j | |
176 ≈⟨ car h-id ⟩ | |
177 id1 A c' o j | |
178 ≈⟨ idL ⟩ | |
179 j | |
180 ∎ | |
181 | |
225 | 182 -- If we have equalizer f g, e fh gh is also equalizer if we have isomorphic pair (same as above) |
183 -- | |
217 | 184 -- e eqa f g f |
185 -- c ----------> a ------->b | |
218 | 186 -- ^ ---> d ---> |
187 -- | i h | |
188 -- j| k' (d' → d) | |
189 -- | k (d' → a) | |
190 -- d' | |
217 | 191 |
218 | 192 equalizer+h : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (i : Hom A c d ) → (h : Hom A d a ) → (h-1 : Hom A a d ) |
193 → A [ A [ h o i ] ≈ e eqa ] → A [ A [ h-1 o h ] ≈ id1 A d ] | |
217 | 194 → Equalizer A {c} (A [ f o h ]) (A [ g o h ] ) |
218 | 195 equalizer+h {a} {b} {c} {d} {f} {g} eqa i h h-1 eq h-1-id = record { |
196 e = i ; -- A [ h-1 o e eqa ] ; -- Hom A a d | |
221 | 197 fe=ge = fe=ge1 ; |
217 | 198 k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ; |
199 ek=h = ek=h1 ; | |
200 uniqueness = uniqueness1 | |
201 } where | |
202 fhj=ghj : {d' : Obj A } → (j : Hom A d' d ) → | |
203 A [ A [ A [ f o h ] o j ] ≈ A [ A [ g o h ] o j ] ] → | |
204 A [ A [ f o A [ h o j ] ] ≈ A [ g o A [ h o j ] ] ] | |
205 fhj=ghj j eq' = let open ≈-Reasoning (A) in | |
206 begin | |
207 f o ( h o j ) | |
208 ≈⟨ assoc ⟩ | |
209 (f o h ) o j | |
210 ≈⟨ eq' ⟩ | |
211 (g o h ) o j | |
212 ≈↑⟨ assoc ⟩ | |
213 g o ( h o j ) | |
214 ∎ | |
221 | 215 fe=ge1 : A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ] |
216 fe=ge1 = let open ≈-Reasoning (A) in | |
217 | 217 begin |
218 ( f o h ) o i | |
219 ≈↑⟨ assoc ⟩ | |
220 f o (h o i ) | |
221 ≈⟨ cdr eq ⟩ | |
222 f o (e eqa) | |
221 | 223 ≈⟨ fe=ge eqa ⟩ |
217 | 224 g o (e eqa) |
225 ≈↑⟨ cdr eq ⟩ | |
226 g o (h o i ) | |
227 ≈⟨ assoc ⟩ | |
228 ( g o h ) o i | |
229 ∎ | |
218 | 230 ek=h1 : {d' : Obj A} {k' : Hom A d' d} {eq' : A [ A [ A [ f o h ] o k' ] ≈ A [ A [ g o h ] o k' ] ]} → |
231 A [ A [ i o k eqa (A [ h o k' ]) (fhj=ghj k' eq') ] ≈ k' ] | |
232 ek=h1 {d'} {k'} {eq'} = let open ≈-Reasoning (A) in | |
217 | 233 begin |
218 | 234 i o k eqa (h o k' ) (fhj=ghj k' eq') -- h-1 (h o i ) o k eqa (h o k' ) = h-1 (h o k') |
235 ≈↑⟨ idL ⟩ | |
236 (id1 A d ) o ( i o k eqa (h o k' ) (fhj=ghj k' eq')) | |
237 ≈↑⟨ car h-1-id ⟩ | |
238 ( h-1 o h ) o ( i o k eqa (h o k' ) (fhj=ghj k' eq')) | |
239 ≈↑⟨ assoc ⟩ | |
240 h-1 o ( h o ( i o k eqa (h o k' ) (fhj=ghj k' eq')) ) | |
241 ≈⟨ cdr assoc ⟩ | |
242 h-1 o ( (h o i ) o k eqa (h o k' ) (fhj=ghj k' eq')) | |
243 ≈⟨ cdr (car eq ) ⟩ | |
244 h-1 o ( (e eqa) o k eqa (h o k' ) (fhj=ghj k' eq')) | |
245 ≈⟨ cdr (ek=h eqa) ⟩ | |
246 h-1 o ( h o k' ) | |
247 ≈⟨ assoc ⟩ | |
248 ( h-1 o h ) o k' | |
249 ≈⟨ car h-1-id ⟩ | |
250 id1 A d o k' | |
251 ≈⟨ idL ⟩ | |
252 k' | |
217 | 253 ∎ |
254 uniqueness1 : {d' : Obj A} {h' : Hom A d' d} {eq' : A [ A [ A [ f o h ] o h' ] ≈ A [ A [ g o h ] o h' ] ]} {k' : Hom A d' c} → | |
255 A [ A [ i o k' ] ≈ h' ] → A [ k eqa (A [ h o h' ]) (fhj=ghj h' eq') ≈ k' ] | |
256 uniqueness1 {d'} {h'} {eq'} {k'} ik=h = let open ≈-Reasoning (A) in | |
257 begin | |
258 k eqa (A [ h o h' ]) (fhj=ghj h' eq') | |
259 ≈⟨ uniqueness eqa ( begin | |
260 e eqa o k' | |
261 ≈↑⟨ car eq ⟩ | |
262 (h o i ) o k' | |
263 ≈↑⟨ assoc ⟩ | |
264 h o (i o k') | |
265 ≈⟨ cdr ik=h ⟩ | |
266 h o h' | |
267 ∎ ) ⟩ | |
268 k' | |
269 ∎ | |
215 | 270 |
225 | 271 -- If we have equalizer f g, e hf hg is also equalizer if we have isomorphic pair |
272 | |
218 | 273 h+equalizer : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) (h : Hom A b d ) |
274 → (h-1 : Hom A d b ) → A [ A [ h-1 o h ] ≈ id1 A b ] | |
275 → Equalizer A {c} (A [ h o f ]) (A [ h o g ] ) | |
276 h+equalizer {a} {b} {c} {d} {f} {g} eqa h h-1 h-1-id = record { | |
277 e = e eqa ; | |
221 | 278 fe=ge = fe=ge1 ; |
218 | 279 k = λ j eq' → k eqa j (fj=gj j eq') ; |
280 ek=h = ek=h1 ; | |
281 uniqueness = uniqueness1 | |
282 } where | |
283 fj=gj : {e : Obj A} → (j : Hom A e a ) → A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ] → A [ A [ f o j ] ≈ A [ g o j ] ] | |
284 fj=gj j eq = let open ≈-Reasoning (A) in | |
285 begin | |
286 f o j | |
287 ≈↑⟨ idL ⟩ | |
288 id1 A b o ( f o j ) | |
289 ≈↑⟨ car h-1-id ⟩ | |
290 (h-1 o h ) o ( f o j ) | |
291 ≈↑⟨ assoc ⟩ | |
292 h-1 o (h o ( f o j )) | |
293 ≈⟨ cdr assoc ⟩ | |
294 h-1 o ((h o f) o j ) | |
295 ≈⟨ cdr eq ⟩ | |
296 h-1 o ((h o g) o j ) | |
297 ≈↑⟨ cdr assoc ⟩ | |
298 h-1 o (h o ( g o j )) | |
299 ≈⟨ assoc ⟩ | |
300 (h-1 o h) o ( g o j ) | |
301 ≈⟨ car h-1-id ⟩ | |
302 id1 A b o ( g o j ) | |
303 ≈⟨ idL ⟩ | |
304 g o j | |
305 ∎ | |
221 | 306 fe=ge1 : A [ A [ A [ h o f ] o e eqa ] ≈ A [ A [ h o g ] o e eqa ] ] |
307 fe=ge1 = let open ≈-Reasoning (A) in | |
218 | 308 begin |
309 ( h o f ) o e eqa | |
310 ≈↑⟨ assoc ⟩ | |
311 h o (f o e eqa ) | |
221 | 312 ≈⟨ cdr (fe=ge eqa) ⟩ |
218 | 313 h o (g o e eqa ) |
314 ≈⟨ assoc ⟩ | |
315 ( h o g ) o e eqa | |
316 ∎ | |
317 ek=h1 : {d₁ : Obj A} {j : Hom A d₁ a} {eq : A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ]} → | |
318 A [ A [ e eqa o k eqa j (fj=gj j eq) ] ≈ j ] | |
319 ek=h1 {d₁} {j} {eq} = ek=h eqa | |
320 uniqueness1 : {d₁ : Obj A} {j : Hom A d₁ a} {eq : A [ A [ A [ h o f ] o j ] ≈ A [ A [ h o g ] o j ] ]} {k' : Hom A d₁ c} → | |
321 A [ A [ e eqa o k' ] ≈ j ] → A [ k eqa j (fj=gj j eq) ≈ k' ] | |
322 uniqueness1 = uniqueness eqa | |
323 | |
225 | 324 -- If we have equalizer f g, e (ef) (eg) is also an equalizer and e = id c |
325 | |
220 | 326 eefeg : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) |
327 → Equalizer A {c} (A [ f o e eqa ]) (A [ g o e eqa ] ) | |
328 eefeg {a} {b} {c} {d} {f} {g} eqa = record { | |
329 e = id1 A c ; -- i ; -- A [ h-1 o e eqa ] ; -- Hom A a d | |
221 | 330 fe=ge = fe=ge1 ; |
220 | 331 k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ; |
332 ek=h = ek=h1 ; | |
333 uniqueness = uniqueness1 | |
334 } where | |
335 i = id1 A c | |
336 h = e eqa | |
337 fhj=ghj : {d' : Obj A } → (j : Hom A d' c ) → | |
338 A [ A [ A [ f o h ] o j ] ≈ A [ A [ g o h ] o j ] ] → | |
339 A [ A [ f o A [ h o j ] ] ≈ A [ g o A [ h o j ] ] ] | |
340 fhj=ghj j eq' = let open ≈-Reasoning (A) in | |
341 begin | |
342 f o ( h o j ) | |
343 ≈⟨ assoc ⟩ | |
344 (f o h ) o j | |
345 ≈⟨ eq' ⟩ | |
346 (g o h ) o j | |
347 ≈↑⟨ assoc ⟩ | |
348 g o ( h o j ) | |
349 ∎ | |
221 | 350 fe=ge1 : A [ A [ A [ f o h ] o i ] ≈ A [ A [ g o h ] o i ] ] |
351 fe=ge1 = let open ≈-Reasoning (A) in | |
220 | 352 begin |
353 ( f o h ) o i | |
221 | 354 ≈⟨ car ( fe=ge eqa ) ⟩ |
220 | 355 ( g o h ) o i |
356 ∎ | |
357 ek=h1 : {d' : Obj A} {k' : Hom A d' c} {eq' : A [ A [ A [ f o h ] o k' ] ≈ A [ A [ g o h ] o k' ] ]} → | |
358 A [ A [ i o k eqa (A [ h o k' ]) (fhj=ghj k' eq') ] ≈ k' ] | |
359 ek=h1 {d'} {k'} {eq'} = let open ≈-Reasoning (A) in | |
360 begin | |
361 i o k eqa (h o k' ) (fhj=ghj k' eq') -- h-1 (h o i ) o k eqa (h o k' ) = h-1 (h o k') | |
362 ≈⟨ idL ⟩ | |
363 k eqa (e eqa o k' ) (fhj=ghj k' eq') | |
364 ≈⟨ uniqueness eqa refl-hom ⟩ | |
365 k' | |
366 ∎ | |
367 uniqueness1 : {d' : Obj A} {h' : Hom A d' c} {eq' : A [ A [ A [ f o h ] o h' ] ≈ A [ A [ g o h ] o h' ] ]} {k' : Hom A d' c} → | |
368 A [ A [ i o k' ] ≈ h' ] → A [ k eqa (A [ h o h' ]) (fhj=ghj h' eq') ≈ k' ] | |
369 uniqueness1 {d'} {h'} {eq'} {k'} ik=h = let open ≈-Reasoning (A) in | |
370 begin | |
371 k eqa ( e eqa o h') (fhj=ghj h' eq') | |
372 ≈⟨ uniqueness eqa ( begin | |
373 e eqa o k' | |
374 ≈↑⟨ cdr idL ⟩ | |
375 e eqa o (id1 A c o k' ) | |
376 ≈⟨ cdr ik=h ⟩ | |
377 e eqa o h' | |
378 ∎ ) ⟩ | |
379 k' | |
380 ∎ | |
381 | |
225 | 382 -- |
383 -- If we have two equalizers on c and c', there are isomorphic pair h, h' | |
384 -- | |
385 -- h : c → c' h' : c' → c | |
386 -- | |
387 -- not yet done | |
388 | |
389 | |
223 | 390 iso-rev : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {c} f g) → Hom A a c |
224 | 391 iso-rev {a} {b} {c} {f} {g} eq eqa = k eqa (id1 A a) (f1=g1 eq (id1 A a)) |
223 | 392 |
224 | 393 equalizer-iso-pair : { a b c : Obj A } {f g : Hom A a b } → {eq : A [ f ≈ g ] } → ( eqa : Equalizer A {c} f g) → |
223 | 394 A [ A [ e eqa o iso-rev eq eqa ] ≈ id1 A a ] |
224 | 395 equalizer-iso-pair {a} {b} {c} {f} {g} {eq} eqa = ek=h eqa |
223 | 396 |
221 | 397 -- Equalizer is unique up to iso |
398 | |
399 equalizer-iso : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) | |
400 → Hom A c c' --- != id1 A c | |
401 equalizer-iso {c} eqa eqa' = k eqa' (e eqa) (fe=ge eqa) | |
220 | 402 |
221 | 403 -- |
404 -- | |
405 -- e eqa f g f | |
406 -- c ----------> a ------->b | |
407 -- | |
224 | 408 equalizer-iso-eq' : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) |
222 | 409 { h : Hom A a c } → A [ A [ h o e eqa ] ≈ id1 A c ] → A [ A [ k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) ] ≈ id1 A c ] |
224 | 410 equalizer-iso-eq' {c} {c'} {f} {g} eqa eqa' {h} rev = let open ≈-Reasoning (A) in |
221 | 411 begin |
222 | 412 k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) |
413 ≈↑⟨ idL ⟩ | |
414 (id1 A c) o ( k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) ) | |
415 ≈↑⟨ car rev ⟩ | |
416 ( h o e eqa ) o ( k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) ) | |
417 ≈↑⟨ assoc ⟩ | |
418 h o ( e eqa o ( k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) ) ) | |
419 ≈⟨ cdr assoc ⟩ | |
420 h o (( e eqa o k eqa (e eqa' ) (fe=ge eqa')) o k eqa' (e eqa ) (fe=ge eqa) ) | |
421 ≈⟨ cdr ( car (ek=h eqa) ) ⟩ | |
422 h o ( e eqa' o k eqa' (e eqa ) (fe=ge eqa) ) | |
423 ≈⟨ cdr (ek=h eqa' ) ⟩ | |
424 h o e eqa | |
425 ≈⟨ rev ⟩ | |
426 id1 A c | |
221 | 427 ∎ |
428 | |
225 | 429 equalizer-iso-eq : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) |
430 → A [ A [ k eqa (e eqa' ) (fe=ge eqa') o k eqa' (e eqa ) (fe=ge eqa) ] ≈ id1 A c ] | |
431 equalizer-iso-eq {c} {c'} {f} {g} eqa eqa' = equalizer-iso-eq' {c} {c'} {f} {g} eqa eqa' {{!!}} {!!} | |
432 | |
221 | 433 -- ke = e' k'e' = e → k k' = 1 , k' k = 1 |
434 -- ke = e' | |
435 -- k'ke = k'e' = e kk' = 1 | |
436 -- x e = e -> x = id? | |
218 | 437 |
225 | 438 ---- |
439 -- | |
440 -- An equalizer satisfies Burroni equations | |
441 -- | |
442 -- b4 is not yet done | |
443 ---- | |
444 | |
222 | 445 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → |
225 | 446 ( {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → Burroni A {c} f g |
222 | 447 lemma-equ1 {a} {b} {c} f g eqa = record { |
216 | 448 α = λ f g → e (eqa f g ) ; -- Hom A c a |
214 | 449 γ = λ {a} {b} {c} {d} f g h → k (eqa f g ) {d} ( A [ h o (e ( eqa (A [ f o h ] ) (A [ g o h ] ))) ] ) (lemma-equ4 {a} {b} {c} {d} f g h ) ; -- Hom A c d |
213 | 450 δ = λ {a} f → k (eqa f f) (id1 A a) (lemma-equ2 f); -- Hom A a c |
221 | 451 b1 = fe=ge (eqa f g) ; |
212 | 452 b2 = lemma-equ5 ; |
453 b3 = lemma-equ3 ; | |
215 | 454 b4 = lemma-equ6 |
211 | 455 } where |
216 | 456 -- |
457 -- e eqa f g f | |
458 -- c ----------> a ------->b | |
459 -- ^ g | |
460 -- | | |
461 -- |k₁ = e eqa (f o (e (eqa f g))) (g o (e (eqa f g)))) | |
462 -- | | |
463 -- d | |
464 -- | |
465 -- | |
466 -- e o id1 ≈ e → k e ≈ id | |
467 | |
211 | 468 lemma-equ2 : {a b : Obj A} (f : Hom A a b) → A [ A [ f o id1 A a ] ≈ A [ f o id1 A a ] ] |
469 lemma-equ2 f = let open ≈-Reasoning (A) in refl-hom | |
213 | 470 lemma-equ3 : A [ A [ e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) ] ≈ id1 A a ] |
471 lemma-equ3 = let open ≈-Reasoning (A) in | |
211 | 472 begin |
473 e (eqa f f) o k (eqa f f) (id1 A a) (lemma-equ2 f) | |
215 | 474 ≈⟨ ek=h (eqa f f ) ⟩ |
211 | 475 id1 A a |
476 ∎ | |
214 | 477 lemma-equ4 : {a b c d : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → |
212 | 478 A [ A [ f o A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ] ] |
214 | 479 lemma-equ4 {a} {b} {c} {d} f g h = let open ≈-Reasoning (A) in |
212 | 480 begin |
481 f o ( h o e (eqa (f o h) ( g o h ))) | |
482 ≈⟨ assoc ⟩ | |
483 (f o h) o e (eqa (f o h) ( g o h )) | |
221 | 484 ≈⟨ fe=ge (eqa (A [ f o h ]) (A [ g o h ])) ⟩ |
212 | 485 (g o h) o e (eqa (f o h) ( g o h )) |
486 ≈↑⟨ assoc ⟩ | |
487 g o ( h o e (eqa (f o h) ( g o h ))) | |
488 ∎ | |
489 lemma-equ5 : {d : Obj A} {h : Hom A d a} → A [ | |
214 | 490 A [ e (eqa f g) o k (eqa f g) (A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ]) (lemma-equ4 {a} {b} {c} f g h) ] |
212 | 491 ≈ A [ h o e (eqa (A [ f o h ]) (A [ g o h ])) ] ] |
492 lemma-equ5 {d} {h} = let open ≈-Reasoning (A) in | |
493 begin | |
215 | 494 e (eqa f g) o k (eqa f g) (h o e (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} {c} f g h) |
495 ≈⟨ ek=h (eqa f g) ⟩ | |
212 | 496 h o e (eqa (f o h ) ( g o h )) |
497 ∎ | |
222 | 498 lemma-equ6 : {d : Obj A} {j : Hom A d c} → A [ |
499 A [ k (eqa f g) (A [ A [ e (eqa f g) o j ] o e (eqa (A [ f o A [ e (eqa f g) o j ] ]) (A [ g o A [ e (eqa f g) o j ] ])) ]) | |
500 (lemma-equ4 {a} {b} {c} f g (A [ e (eqa f g) o j ])) o | |
501 k (eqa (A [ f o A [ e (eqa f g) o j ] ]) (A [ f o A [ e (eqa f g) o j ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ e (eqa f g) o j ] ])) ] | |
502 ≈ j ] | |
503 lemma-equ6 {d} {j} = let open ≈-Reasoning (A) in | |
215 | 504 begin |
222 | 505 ( k (eqa f g) (( ( e (eqa f g) o j ) o e (eqa (( f o ( e (eqa f g) o j ) )) (( g o ( e (eqa f g) o j ) ))) )) |
506 (lemma-equ4 {a} {b} {c} f g (( e (eqa f g) o j ))) o | |
507 k (eqa (( f o ( e (eqa f g) o j ) )) (( f o ( e (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o j ) ))) ) | |
215 | 508 ≈⟨ car ( uniqueness (eqa f g) ( begin |
222 | 509 e (eqa f g) o j |
215 | 510 ≈⟨ {!!} ⟩ |
222 | 511 (e (eqa f g) o j) o e (eqa (f o e (eqa f g) o j) (g o e (eqa f g) o j)) |
215 | 512 ∎ )) ⟩ |
222 | 513 j o k (eqa (( f o ( e (eqa f g) o j ) )) (( f o ( e (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( e (eqa f g) o j ) ))) |
514 ≈⟨ cdr ( uniqueness (eqa (( f o ( e (eqa f g) o j ) )) (( f o ( e (eqa f g) o j ) ))) ( begin | |
515 e (eqa (f o e (eqa f g) o j) (f o e (eqa f g) o j)) o id1 A d | |
516 ≈⟨ idR ⟩ | |
517 e (eqa (f o e (eqa f g) o j) (f o e (eqa f g) o j)) | |
215 | 518 ≈⟨ {!!} ⟩ |
222 | 519 id1 A d |
215 | 520 ∎ )) ⟩ |
222 | 521 j o id1 A d |
215 | 522 ≈⟨ idR ⟩ |
222 | 523 j |
215 | 524 ∎ |
211 | 525 |
526 | |
225 | 527 -- end |
212 | 528 |
529 | |
530 | |
215 | 531 |
532 |