Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 237:776cda2286c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 08 Sep 2013 05:55:56 +0900
parents e20b81102eee
children c8db99cdf72a
comparison
equal deleted inserted replaced
236:e20b81102eee 237:776cda2286c8
273 equalizer (eqa f g) o k (eqa f g) (h o equalizer (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} {c} f g h) 273 equalizer (eqa f g) o k (eqa f g) (h o equalizer (eqa (f o h) (g o h))) (lemma-equ4 {a} {b} {c} f g h)
274 ≈⟨ ek=h (eqa f g) ⟩ 274 ≈⟨ ek=h (eqa f g) ⟩
275 h o equalizer (eqa (f o h ) ( g o h )) 275 h o equalizer (eqa (f o h ) ( g o h ))
276 ∎ 276 ∎
277 277
278 ------- α(f,g)j id d = α(f,g)j
279 ------- α(f,g)j id d = α(f,g)j
280 ------- α(f,g)j α(fα(f,g)j,fα(f,g)j) δ(fα(f,g)j) = α(f,g)j
281 ------ fα = gα
282 ------- α(f,g)j α(fα(f,g)j,gα(f,g)j) δ(fα(f,g)j) = α(f,g)j
283 ------- α(f,g) γ(f,g,α(f,g)j) δ(fα(f,g)j) = α(f,g)j
284 ------- γ(f,g,α(f,g)j) δ(fα(f,g)j) = j
285
286 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 {id1 A a}) ] ) (A [ g o equalizer (eqa f g {id1 A a}) ] )
287 eefg f g {e} = eqa ( A [ f o equalizer (eqa f g) ] ) (A [ g o equalizer (eqa f g) ] )
288 lemma-b4 : {d : Obj A} {j : Hom A d c} → A [ 278 lemma-b4 : {d : Obj A} {j : Hom A d c} → A [
289 A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o 279 A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o
290 equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ]) 280 equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ])
291 (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o 281 (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o
292 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 ] ])) ] 282 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 ] ])) ]