Mercurial > hg > Members > kono > Proof > category
comparison equalizer.agda @ 235:8835015a3e1a
passed let;s remove yellow
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 08 Sep 2013 04:55:01 +0900 |
parents | c02287d3d2dc |
children | e20b81102eee |
comparison
equal
deleted
inserted
replaced
234:c02287d3d2dc | 235:8835015a3e1a |
---|---|
180 ∎ | 180 ∎ |
181 | 181 |
182 c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) | 182 c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) |
183 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ]) (A [ g o e' ]) ) | 183 → ( keqa : Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ]) (A [ g o e' ]) ) |
184 → ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ]) (A [ g o e ]) ) | 184 → ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ]) (A [ g o e ]) ) |
185 → { e'->e : A [ e' ≈ A [ e o equalizer keqa' ] ] } | 185 → { e'->e : A [ e' ≈ A [ e o equalizer keqa' ] ] } -- refl |
186 → A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ] ≈ id1 A c ] | 186 → A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ] ≈ id1 A c ] |
187 c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' {e'->e} = let open ≈-Reasoning (A) in begin | 187 c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' {e'->e} = let open ≈-Reasoning (A) in begin |
188 c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa | 188 c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa |
189 ≈⟨⟩ | 189 ≈⟨⟩ |
190 k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) o k eqa' e (fe=ge eqa ) | 190 k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) o k eqa' e (fe=ge eqa ) |
280 ------ fα = gα | 280 ------ fα = gα |
281 ------- α(f,g)j α(fα(f,g)j,gα(f,g)j) δ(fα(f,g)j) = α(f,g)j | 281 ------- α(f,g)j α(fα(f,g)j,gα(f,g)j) δ(fα(f,g)j) = α(f,g)j |
282 ------- α(f,g) γ(f,g,α(f,g)j) δ(fα(f,g)j) = α(f,g)j | 282 ------- α(f,g) γ(f,g,α(f,g)j) δ(fα(f,g)j) = α(f,g)j |
283 ------- γ(f,g,α(f,g)j) δ(fα(f,g)j) = j | 283 ------- γ(f,g,α(f,g)j) δ(fα(f,g)j) = j |
284 | 284 |
285 eefg : {a b c : Obj A} (f g : Hom A a b) {e : Hom A c a} → Equalizer A e ( A [ f o equalizer (eqa f g) ] ) (A [ g o equalizer (eqa f g) ] ) | |
286 eefg f g {e} = eqa ( A [ f o equalizer (eqa f g) ] ) (A [ g o equalizer (eqa f g) ] ) | |
285 lemma-b4 : {d : Obj A} {j : Hom A d c} → A [ | 287 lemma-b4 : {d : Obj A} {j : Hom A d c} → A [ |
286 A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o equalizer (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ g o A [ equalizer (eqa f g) o j ] ])) ]) | 288 A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o equalizer (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ g o A [ equalizer (eqa f g) o j ] ])) ]) |
287 (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o | 289 (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o |
288 k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ equalizer (eqa f g) o j ] ])) ] | 290 k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ])) (id1 A d) (lemma-equ2 (A [ f o A [ equalizer (eqa f g) o j ] ])) ] |
289 ≈ j ] | 291 ≈ j ] |
290 lemma-b4 {d} {j} = let open ≈-Reasoning (A) in | 292 lemma-b4 {d} {j} = let open ≈-Reasoning (A) in |
291 begin | 293 begin |
292 ( k (eqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g) o j ) )) (( g o ( equalizer (eqa f g) o j ) ))) )) | 294 ( k (eqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g) o j ) )) (( g o ( equalizer (eqa f g) o j ) ))) )) |
293 (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o j ))) o | 295 (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o j ))) o |
294 k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) ) | 296 k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) ) |
295 ≈⟨ {!!} ⟩ | 297 ≈⟨ car ((uniqueness (eqa f g) ( begin |
298 equalizer (eqa f g) o j | |
299 ≈↑⟨ idR ⟩ | |
300 (equalizer (eqa f g) o j ) o id1 A d | |
301 ≈⟨⟩ | |
302 ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g) o j) (g o equalizer (eqa f g) o j))) | |
303 ∎ ))) ⟩ | |
304 j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (lemma-equ2 (( f o ( equalizer (eqa f g) o j ) ))) | |
305 ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) ( begin | |
306 equalizer (eqa (f o equalizer (eqa f g) o j) (f o equalizer (eqa f g) o j)) | |
307 ≈⟨ {!!} ⟩ | |
308 id1 A d | |
309 ∎ ))) ⟩ | |
310 j o id1 A d | |
311 ≈⟨ idR ⟩ | |
296 j | 312 j |
297 ∎ | 313 ∎ |
298 | 314 |
299 | 315 |
300 -- end | 316 -- end |
301 | 317 |
302 | 318 |