Mercurial > hg > Members > kono > Proof > category
changeset 252:e0835b8dd51b
comment
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 09 Sep 2013 16:15:09 +0900 |
| parents | 40947f08bab6 |
| children | 24e83b8b81be |
| files | equalizer.agda |
| diffstat | 1 files changed, 3 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Mon Sep 09 16:03:14 2013 +0900 +++ b/equalizer.agda Mon Sep 09 16:15:09 2013 +0900 @@ -209,6 +209,9 @@ e' ∎ +-- e←e' e'←e = e +-- e'←e e←e = e' is enough for isomorphism but we want to prove l o r = id also. + 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' ]