Mercurial > hg > Members > kono > Proof > category
changeset 237:776cda2286c8
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 08 Sep 2013 05:55:56 +0900 |
| parents | e20b81102eee |
| children | c8db99cdf72a |
| files | equalizer.agda |
| diffstat | 1 files changed, 0 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Sun Sep 08 05:54:27 2013 +0900 +++ b/equalizer.agda Sun Sep 08 05:55:56 2013 +0900 @@ -275,16 +275,6 @@ h o equalizer (eqa (f o h ) ( g o h )) ∎ - ------- α(f,g)j id d = α(f,g)j - ------- α(f,g)j id d = α(f,g)j - ------- α(f,g)j α(fα(f,g)j,fα(f,g)j) δ(fα(f,g)j) = α(f,g)j - ------ fα = gα - ------- α(f,g)j α(fα(f,g)j,gα(f,g)j) δ(fα(f,g)j) = α(f,g)j - ------- α(f,g) γ(f,g,α(f,g)j) δ(fα(f,g)j) = α(f,g)j - ------- γ(f,g,α(f,g)j) δ(fα(f,g)j) = j - - 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}) ] ) - eefg f g {e} = eqa ( A [ f o equalizer (eqa f g) ] ) (A [ g o equalizer (eqa f g) ] ) lemma-b4 : {d : Obj A} {j : Hom A d c} → A [ A [ k (eqa f g) (A [ A [ equalizer (eqa f g) o j ] o equalizer (eqa (A [ f o A [ equalizer (eqa f g {e}) o j ] ]) (A [ g o A [ equalizer (eqa f g {e} ) o j ] ])) ])