Mercurial > hg > Members > kono > Proof > category
changeset 232:b0fe61882014
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 07 Sep 2013 23:29:13 +0900 |
| parents | 1dc1c697145f |
| children | 4bba19bc71be |
| files | equalizer.agda |
| diffstat | 1 files changed, 9 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Sat Sep 07 23:14:05 2013 +0900 +++ b/equalizer.agda Sat Sep 07 23:29:13 2013 +0900 @@ -445,14 +445,21 @@ -- ((k (eff) id1a )) o k α e = id1 A c +reverse-e' : {a b c : Obj A} (f g : Hom A a b) → (h i : Hom A c b ) → + ( eqa : {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → + A [ k (eqa f f ) (id1 A a ) ( f1=f1 f ) ≈ (e (eqa (A [ f o e (eqa f g) ]) (A [ g o e (eqa f g) ]))) ] +reverse-e' = ? + reverse-e : {a b c : Obj A} (f g : Hom A a b) → (h i : Hom A c b ) → ( eqa : {a b c : Obj A} → (f g : Hom A a b) → Equalizer A {c} f g ) → A [ - A [ e (eqa ( A [ f o (e (eqa f g)) ] ) (A [ g o (e (eqa f g )) ] )) o k (eqa ( A [ f o (e (eqa f g)) ] ) (A [ g o (e (eqa f g )) ] )) (id1 A c) {!!} ] + A [ k (eqa f f ) (id1 A a ) ( f1=f1 f ) o k (eqa ( A [ f o (e (eqa f g)) ] ) (A [ g o (e (eqa f g )) ] )) (id1 A c) (f1=g1 (fe=ge (eqa f g)) (id1 A c)) ] ≈ id1 A c ] reverse-e {a} {b} {c} f g h i eqa = let open ≈-Reasoning (A) in begin - e (eqa ( A [ f o (e (eqa f g)) ] ) (A [ g o (e (eqa f g )) ] )) o k (eqa ( A [ f o (e (eqa f g)) ] ) (A [ g o (e (eqa f g )) ] )) (id1 A c) {!!} + k (eqa f f ) (id1 A a ) (f1=f1 f) o k (eqa ( A [ f o (e (eqa f g)) ] ) (A [ g o (e (eqa f g )) ] )) (id1 A c) {!!} + ≈⟨ car {!!} ⟩ + e (eqa ( A [ f o (e (eqa f g)) ] ) (A [ g o (e (eqa f g )) ] )) o k (eqa ( A [ f o (e (eqa f g)) ] ) (A [ g o (e (eqa f g )) ] )) (id1 A c) (f1=g1 (fe=ge (eqa f g)) (id1 A c)) ≈⟨ ek=h (eqa ( A [ f o (e (eqa f g)) ] ) (A [ g o (e (eqa f g )) ] )) ⟩ id1 A c ∎