Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 227:591efd381c82

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 21:34:33 +0900
parents 27f2c77c963f
children ff596cff8183
comparison
equal deleted inserted replaced
226:27f2c77c963f 227:591efd381c82
47 -- A [ α f g o β f g h ] ≈ h 47 -- A [ α f g o β f g h ] ≈ h
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 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 ]) ] 49 β {d} {e} {a} {b} f g h = A [ γ {a} {b} {c} f g h o δ (A [ f o h ]) ]
50 50
51 open Equalizer 51 open Equalizer
52
52 open Burroni 53 open Burroni
53 54
54 -- 55 --
55 -- Some obvious conditions for k (fe = ge) → ( fh = gh ) 56 -- Some obvious conditions for k (fe = ge) → ( fh = gh )
56 -- 57 --
324 A [ A [ e eqa o k' ] ≈ j ] → A [ k eqa j (fj=gj j eq) ≈ k' ] 325 A [ A [ e eqa o k' ] ≈ j ] → A [ k eqa j (fj=gj j eq) ≈ k' ]
325 uniqueness1 = uniqueness eqa 326 uniqueness1 = uniqueness eqa
326 327
327 -- If we have equalizer f g, e (ef) (eg) is also an equalizer and e = id c 328 -- If we have equalizer f g, e (ef) (eg) is also an equalizer and e = id c
328 329
329 eefeg : {a b c d : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g) 330 eefeg : {a b c : Obj A } {f g : Hom A a b } ( eqa : Equalizer A {c} f g)
330 → Equalizer A {c} (A [ f o e eqa ]) (A [ g o e eqa ] ) 331 → Equalizer A {c} (A [ f o e eqa ]) (A [ g o e eqa ] )
331 eefeg {a} {b} {c} {d} {f} {g} eqa = record { 332 eefeg {a} {b} {c} {f} {g} eqa = record {
332 e = id1 A c ; -- i ; -- A [ h-1 o e eqa ] ; -- Hom A a d 333 e = id1 A c ; -- i ; -- A [ h-1 o e eqa ] ; -- Hom A a d
333 fe=ge = fe=ge1 ; 334 fe=ge = fe=ge1 ;
334 k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ; 335 k = λ j eq' → k eqa (A [ h o j ]) (fhj=ghj j eq' ) ;
335 ek=h = ek=h1 ; 336 ek=h = ek=h1 ;
336 uniqueness = uniqueness1 337 uniqueness = uniqueness1
400 → Hom A c' c 401 → Hom A c' c
401 c-iso-r eqa eqa' eff' eff = let open ≈-Reasoning (A) in k eff (e eqa') refl-hom 402 c-iso-r eqa eqa' eff' eff = let open ≈-Reasoning (A) in k eff (e eqa') refl-hom
402 403
403 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 )
404 → (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 )
405 → A [ A [ k eqa' (A [ e eqa' o k eff' (id1 A a ) (f1=f1 f) ] ) (f1=gh ( fe=ge eqa' ) ) o e eff' ] ≈ 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' ]
406 c-iso-1 = {!!} 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'))
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' )⟩
412 id1 A c'
413 ∎
414
415 -- e k e k = 1c e e = e -> e = 1c?
416 -- k e k e = 1c' ?
417
407 418
408 c-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 ) 419 c-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 )
409 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f ) 420 → (eff' : Equalizer A {c'} f f ) → (eff : Equalizer A {c} f f )
410 → A [ A [ c-iso-l eqa eqa' eff' eff o c-iso-r eqa eqa' eff' eff ] ≈ id1 A c' ] 421 → A [ A [ c-iso-l eqa eqa' eff' eff o c-iso-r eqa eqa' eff' eff ] ≈ id1 A c' ]
411 c-iso {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff = let open ≈-Reasoning (A) in begin 422 c-iso {c} {c'} {a} {b} {f} {g} eqa eqa' eff' eff = let open ≈-Reasoning (A) in begin