Mercurial > hg > Members > kono > Proof > category
changeset 223:8b3aeba14b5e
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 05 Sep 2013 04:35:22 +0900 |
| parents | 0bc85361b7d0 |
| children | a9d311cea336 |
| files | equalizer.agda |
| diffstat | 1 files changed, 7 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Thu Sep 05 01:23:53 2013 +0900 +++ b/equalizer.agda Thu Sep 05 04:35:22 2013 +0900 @@ -346,6 +346,13 @@ k' ∎ +iso-rev : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {c} f g) → Hom A a c +iso-rev {a} {b} {c} {f} {g} eq eqa = k eqa (id1 A a) (f1=g1 eq) + +equalizer-iso-pair : { a b c : Obj A } {f g : Hom A a b } → (eq : A [ f ≈ g ] ) → ( eqa : Equalizer A {c} f g) → + A [ A [ e eqa o iso-rev eq eqa ] ≈ id1 A a ] +equalizer-iso-pair {a} {b} {c} {f} {g} eq eqa = ek=h eqa + -- Equalizer is unique up to iso equalizer-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 )