Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 254:45b81fcb8a64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalizer fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Sep 2013 10:04:18 +0900
parents 24e83b8b81be
children 7e7b2c38dee1
comparison
equal deleted inserted replaced
253:24e83b8b81be 254:45b81fcb8a64
94 -- c' 94 -- c'
95 95
96 equalizer+iso : {a b c c' : Obj A } {f g : Hom A a b } {e : Hom A c a } 96 equalizer+iso : {a b c c' : Obj A } {f g : Hom A a b } {e : Hom A c a }
97 (h-1 : Hom A c' c ) → (h : Hom A c c' ) → 97 (h-1 : Hom A c' c ) → (h : Hom A c c' ) →
98 A [ A [ h o h-1 ] ≈ id1 A c' ] → A [ A [ h-1 o h ] ≈ id1 A c ] → 98 A [ A [ h o h-1 ] ≈ id1 A c' ] → A [ A [ h-1 o h ] ≈ id1 A c ] →
99 ( fe=ge' : A [ A [ f o A [ e o h-1 ] ] ≈ A [ g o A [ e o h-1 ] ] ] )
100 ( eqa : Equalizer A e f g ) 99 ( eqa : Equalizer A e f g )
101 → Equalizer A (A [ e o h-1 ] ) f g 100 → Equalizer A (A [ e o h-1 ] ) f g
102 equalizer+iso {a} {b} {c} {c'} {f} {g} {e} h-1 h hh-1=1 h-1h=1 fe=ge' eqa = record { 101 equalizer+iso {a} {b} {c} {c'} {f} {g} {e} h-1 h hh-1=1 h-1h=1 eqa = record {
103 fe=ge = fe=ge1 ; 102 fe=ge = fe=ge1 ;
104 k = λ j eq → A [ h o k eqa j eq ] ; 103 k = λ j eq → A [ h o k eqa j eq ] ;
105 ek=h = ek=h1 ; 104 ek=h = ek=h1 ;
106 uniqueness = uniqueness1 105 uniqueness = uniqueness1
107 } where 106 } where
108 fe=ge1 : A [ A [ f o A [ e o h-1 ] ] ≈ A [ g o A [ e o h-1 ] ] ] 107 fe=ge1 : A [ A [ f o A [ e o h-1 ] ] ≈ A [ g o A [ e o h-1 ] ] ]
109 fe=ge1 = fe=ge' 108 fe=ge1 = f1=gh ( fe=ge eqa )
110 ek=h1 : {d : Obj A} {j : Hom A d a} {eq : A [ A [ f o j ] ≈ A [ g o j ] ]} → 109 ek=h1 : {d : Obj A} {j : Hom A d a} {eq : A [ A [ f o j ] ≈ A [ g o j ] ]} →
111 A [ A [ A [ e o h-1 ] o A [ h o k eqa j eq ] ] ≈ j ] 110 A [ A [ A [ e o h-1 ] o A [ h o k eqa j eq ] ] ≈ j ]
112 ek=h1 {d} {j} {eq} = let open ≈-Reasoning (A) in 111 ek=h1 {d} {j} {eq} = let open ≈-Reasoning (A) in
113 begin 112 begin
114 ( e o h-1 ) o ( h o k eqa j eq ) 113 ( e o h-1 ) o ( h o k eqa j eq )
247 ≈⟨ idR ⟩ 246 ≈⟨ idR ⟩
248 e 247 e
249 ∎ )⟩ 248 ∎ )⟩
250 k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) 249 k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) )
251 ∎ )⟩ 250 ∎ )⟩
252 equalizer keqa' o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) ≈⟨ ek=h keqa' ⟩ 251 equalizer keqa' o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) )
252 ≈⟨ ek=h keqa' ⟩
253 id c 253 id c
254 ∎ 254 ∎
255 255
256 256
257 257
258 -------------------------------- 258 --------------------------------
259 ---- 259 ----
260 -- 260 --
261 -- An equalizer satisfies Burroni equations 261 -- Existence of equalizer satisfies Burroni equations
262 -- 262 --
263 ---- 263 ----
264 264
265 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) → 265 lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) →
266 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) 266 ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g )
349 h o equalizer (eqa (f o h ) ( g o h )) 349 h o equalizer (eqa (f o h ) ( g o h ))
350 ∎ 350 ∎
351 351
352 lemma-b4 : {d : Obj A} {j : Hom A d c} → A [ 352 lemma-b4 : {d : Obj A} {j : Hom A d c} → A [
353 A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o 353 A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o
354 equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ]) 354 equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ])
355 (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ])) o 355 (lemma-equ4 {a} {b} {c} f g (A [ equalizer (eqa f g) o j ]))
356 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) (f1=f1 (A [ f o A [ equalizer (eqa f g) o j ] ])) ] 356 o k (eqa (A [ f o A [ equalizer (eqa f g) o j ] ]) (A [ f o A [ equalizer (eqa f g) o j ] ]))
357 (id1 A d) (f1=f1 (A [ f o A [ equalizer (eqa f g) o j ] ])) ]
357 ≈ j ] 358 ≈ j ]
358 lemma-b4 {d} {j} = let open ≈-Reasoning (A) in 359 lemma-b4 {d} {j} = let open ≈-Reasoning (A) in
359 begin 360 begin
360 ( k (eqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g {e}) o j ) )) (( g o ( equalizer (eqa f g {e}) o j ) ))) )) 361 ( k (eqa f g) (( ( equalizer (eqa f g) o j ) o equalizer (eqa (( f o ( equalizer (eqa f g {e}) o j ) )) (( g o ( equalizer (eqa f g {e}) o j ) ))) ))
361 (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o j ))) o 362 (lemma-equ4 {a} {b} {c} f g (( equalizer (eqa f g) o j ))) o