Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 228:ff596cff8183

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 Thu, 05 Sep 2013 22:35:31 +0900
parents 591efd381c82
children 68b2681ea9df
comparison
equal deleted inserted replaced
227:591efd381c82 228:ff596cff8183
392 392
393 393
394 c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) 394 c-iso-l : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g )
395 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f ) 395 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
396 → Hom A c c' 396 → Hom A c c'
397 c-iso-l eqa eqa' eff' eff = let open ≈-Reasoning (A) in k eff' (e eqa) refl-hom 397 c-iso-l {c} {c'} eqa eqa' eff' eff = let open ≈-Reasoning (A) in k eff' (A [ e eqa o id1 A c ]) refl-hom
398 398
399 c-iso-r : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) 399 c-iso-r : { 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 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f ) 400 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
401 → Hom A c' c 401 → Hom A c' c
402 c-iso-r eqa eqa' eff' eff = let open ≈-Reasoning (A) in k eff (e eqa') refl-hom 402 c-iso-r {c} {c'} eqa eqa' eff' eff = let open ≈-Reasoning (A) in k eff (A [ e eqa' o id1 A c' ]) refl-hom
403 403
404 c-iso-1 : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g ) 404 c-iso-1 : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g )
405 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f ) 405 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
406 → A [ A [ e (eefeg eqa') o k (eefeg eqa') (id1 A c') (f1=g1 (fe=ge eqa') (id1 A c')) ] ≈ id1 A c' ] 406 → A [ A [ e (eefeg eqa') o k (eefeg eqa') (id1 A c') (f1=g1 (fe=ge eqa') (id1 A c')) ] ≈ id1 A c' ]
407 c-iso-1 {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff = let open ≈-Reasoning (A) in begin 407 c-iso-1 {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff = let open ≈-Reasoning (A) in begin
408 e (eefeg eqa') o k (eefeg eqa') (id1 A c') (f1=g1 (fe=ge eqa') (id1 A c')) 408 e (eefeg eqa') o k (eefeg eqa') (id1 A c') (f1=g1 (fe=ge eqa') (id1 A c'))
409 ≈⟨ {!!} ⟩
410 e (eefeg eqa') o k (eefeg eqa') (id1 A c') (f1=g1 (fe=ge eqa') (id1 A c'))
411 ≈⟨ ek=h ( eefeg eqa' )⟩ 409 ≈⟨ ek=h ( eefeg eqa' )⟩
410 id1 A c'
411 ∎
412
413 c-iso-2 : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g )
414 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
415 → A [ k eqa' ( A [ e eqa' o id1 A c' ] ) (f1=gh (fe=ge eqa' )) ≈ id1 A c' ]
416 c-iso-2 {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff = let open ≈-Reasoning (A) in begin
417 k eqa' ( A [ e eqa' o id1 A c' ] ) (f1=gh (fe=ge eqa' ) )
418 ≈⟨ uniqueness eqa' refl-hom ⟩
419 id1 A c'
420 ∎
421
422 c-iso-3 : { c c' a b : Obj A } {f g : Hom A a b } → ( eqa : Equalizer A {c} f g) → ( eqa' : Equalizer A {c'} f g )
423 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
424 → A [ k eff' ( A [ e eff' o id1 A c' ] ) (f1=gh (fe=ge eff')) ≈ id1 A c' ]
425 c-iso-3 {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff = let open ≈-Reasoning (A) in begin
426 k eff' ( A [ e eff' o id1 A c' ] ) (f1=gh (fe=ge eff'))
427 ≈⟨ uniqueness eff' refl-hom ⟩
412 id1 A c' 428 id1 A c'
413 ∎ 429 ∎
414 430
415 -- e k e k = 1c e e = e -> e = 1c? 431 -- e k e k = 1c e e = e -> e = 1c?
416 -- k e k e = 1c' ? 432 -- k e k e = 1c' ?
420 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f ) 436 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
421 → A [ A [ c-iso-l eqa eqa' eff' eff o c-iso-r eqa eqa' eff' eff ] ≈ id1 A c' ] 437 → A [ A [ c-iso-l eqa eqa' eff' eff o c-iso-r eqa eqa' eff' eff ] ≈ id1 A c' ]
422 c-iso {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff = let open ≈-Reasoning (A) in begin 438 c-iso {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff = let open ≈-Reasoning (A) in begin
423 c-iso-l eqa eqa' eff' eff o c-iso-r eqa eqa' eff' eff 439 c-iso-l eqa eqa' eff' eff o c-iso-r eqa eqa' eff' eff
424 ≈⟨⟩ 440 ≈⟨⟩
425 k eff' (e eqa) refl-hom o k eff (e eqa') refl-hom 441 k eff' (e eqa o id1 A c) refl-hom o k eff (e eqa' o id1 A c') refl-hom
442 ≈⟨ car ( uniqueness eff' ( begin
443 e eff' o k eff' {!!} {!!}
444 ≈⟨ {!!} ⟩
445 e eqa o id1 A c
446 ∎ )) ⟩
447 {!!} o k eff (e eqa' o id1 A c') refl-hom
426 ≈⟨ {!!} ⟩ 448 ≈⟨ {!!} ⟩
427 id1 A c' 449 id1 A c'
428 ∎ 450 ∎
429 451
430 452