Mercurial > hg > Members > kono > Proof > category
changeset 255:7e7b2c38dee1
every equalizer is monic
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 14 Sep 2013 11:19:12 +0900 |
| parents | 45b81fcb8a64 |
| children | 80dfdeb3e4e7 |
| files | equalizer.agda |
| diffstat | 1 files changed, 29 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/equalizer.agda Sat Sep 14 10:04:18 2013 +0900 +++ b/equalizer.agda Sat Sep 14 11:19:12 2013 +0900 @@ -80,6 +80,34 @@ g o ( e o h ) ∎ +------------------------------- +-- +-- Every equalizer is monic +-- +-- e i = e j → i = j +-- + +monoic : { c a b d : Obj A } {f g : Hom A a b } → {e : Hom A c a } ( eqa : Equalizer A e f g) + → { i j : Hom A d c } + → A [ A [ equalizer eqa o i ] ≈ A [ equalizer eqa o j ] ] → A [ i ≈ j ] +monoic {c} {a} {b} {d} {f} {g} {e} eqa {i} {j} ei=ej = let open ≈-Reasoning (A) in begin + i + ≈↑⟨ uniqueness eqa ( begin + equalizer eqa o i + ≈⟨ ei=ej ⟩ + equalizer eqa o j + ∎ )⟩ + k eqa (equalizer eqa o j) ( f1=gh (fe=ge eqa ) ) + ≈⟨ uniqueness eqa ( begin + equalizer eqa o ( id c o j ) + ≈⟨ cdr idL ⟩ + equalizer eqa o j + ∎ )⟩ + id c o j + ≈⟨ idL ⟩ + j + ∎ + -------------------------------- -- -- @@ -151,6 +179,7 @@ -- h : c → c' h' : c' → c -- e' = h o e -- e = h' o e' +-- we assume equalizer on fe,ge and fe',ge' 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 )