Mercurial > hg > Members > kono > Proof > category
changeset 241:9e4dc349831e
comments
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 08 Sep 2013 12:34:35 +0900 (2013-09-08) |
parents | 964e258e08fb |
children | 5d1ecfec6f41 |
files | equalizer.agda |
diffstat | 1 files changed, 8 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Sun Sep 08 11:54:06 2013 +0900 +++ b/equalizer.agda Sun Sep 08 12:34:35 2013 +0900 @@ -152,12 +152,12 @@ c-iso-l : { 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 ) → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) - → Hom A c c' + → Hom A c c' -- should be e' = c-sio-l o e c-iso-l {c} {c'} eqa eqa' keqa = equalizer keqa c-iso-r : { 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 ) → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) - → Hom A c' c + → Hom A c' c -- e = c-sio-r o e' c-iso-r {c} {c'} eqa eqa' keqa = k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) -- e' f @@ -172,6 +172,7 @@ -- h = j e f -> j = j' -- +-- e = c-iso-l o e' is assumed by equalizer's degree of freedom 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 ) → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) → A [ A [ c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ] ≈ id1 A c' ] @@ -186,7 +187,8 @@ 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 ) → ( keqa : Equalizer A (k eqa' e (fe=ge eqa )) (A [ f o e' ]) (A [ g o e' ]) ) → ( keqa' : Equalizer A (k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') )) (A [ f o e ]) (A [ g o e ]) ) - → { e'->e : A [ e' ≈ A [ e o equalizer keqa' ] ] } -- refl + -- e' = c-iso-r o e is assumed by equalizer's degree of freedom + → { e'->e : A [ e' ≈ A [ e o equalizer keqa' ] ] } -- implicit assumption , which should be refl → A [ A [ c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ] ≈ id1 A c ] c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' {e'->e} = let open ≈-Reasoning (A) in begin c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa @@ -220,7 +222,7 @@ -- -- An equalizer satisfies Burroni equations -- --- b4 is not yet done +-- congs are not yet done ---- lemma-equ1 : {a b c : Obj A} (f g : Hom A a b) → (e : Hom A c a ) → @@ -302,7 +304,7 @@ equalizer (eqa f g) o j ≈↑⟨ idR ⟩ (equalizer (eqa f g) o j ) o id1 A d - ≈⟨⟩ + ≈⟨⟩ -- here we decide e (fej) (gej)' is id1 A d ((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))) ∎ ))) ⟩ 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 ) ))) @@ -310,7 +312,7 @@ equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j)) o id1 A d ≈⟨ idR ⟩ equalizer (eqa (f o equalizer (eqa f g {e}) o j) (f o equalizer (eqa f g {e}) o j)) - ≈⟨⟩ + ≈⟨⟩ -- here we decide e (fej) (fej)' is id1 A d id1 A d ∎ ))) ⟩ j o id1 A d