Mercurial > hg > Members > kono > Proof > category
changeset 205:242adb6669da
equalizer
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 01 Sep 2013 22:10:39 +0900 |
| parents | b2874c5086ea |
| children | 3a5e2a22e053 |
| files | equalizer.agda |
| diffstat | 1 files changed, 30 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/equalizer.agda Sun Sep 01 22:10:39 2013 +0900 @@ -0,0 +1,30 @@ +--- +-- +-- Equalizer +-- +-- f' f +-- c --------> a ----------> b +-- | . ----------> +-- | . g +-- |h . +-- v . g' +-- d +-- +-- Shinji KONO <kono@ie.u-ryukyu.ac.jp> +---- + +open import Category -- https://github.com/konn/category-agda +open import Level +open import Category.Sets +module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where + +open import HomReasoning +open import cat-utility + +record Equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A} (f g : Hom A a b) : Set ( ℓ ⊔ (c₁ ⊔ c₂)) where + field + equalizer : {c d : Obj A} (f' : Hom A c a) (g' : Hom A d a) → Hom A c d + equalize : {c d : Obj A} (f' : Hom A c a) (g' : Hom A d a) → + A [ A [ f o f' ] ≈ A [ A [ g o g' ] o equalizer f' g' ] ] + uniqueness : {c d : Obj A} (f' : Hom A c a) (g' : Hom A d a) ( e : Hom A c d ) → + A [ A [ f o f' ] ≈ A [ A [ g o g' ] o e ] ] → A [ e ≈ equalizer f' g' ]