|
205
|
1 ---
|
|
|
2 --
|
|
|
3 -- Equalizer
|
|
|
4 --
|
|
|
5 -- f' f
|
|
|
6 -- c --------> a ----------> b
|
|
|
7 -- | . ---------->
|
|
|
8 -- | . g
|
|
|
9 -- |h .
|
|
|
10 -- v . g'
|
|
|
11 -- d
|
|
|
12 --
|
|
|
13 -- Shinji KONO <kono@ie.u-ryukyu.ac.jp>
|
|
|
14 ----
|
|
|
15
|
|
|
16 open import Category -- https://github.com/konn/category-agda
|
|
|
17 open import Level
|
|
|
18 open import Category.Sets
|
|
|
19 module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where
|
|
|
20
|
|
|
21 open import HomReasoning
|
|
|
22 open import cat-utility
|
|
|
23
|
|
|
24 record Equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A} (f g : Hom A a b) : Set ( ℓ ⊔ (c₁ ⊔ c₂)) where
|
|
|
25 field
|
|
|
26 equalizer : {c d : Obj A} (f' : Hom A c a) (g' : Hom A d a) → Hom A c d
|
|
|
27 equalize : {c d : Obj A} (f' : Hom A c a) (g' : Hom A d a) →
|
|
|
28 A [ A [ f o f' ] ≈ A [ A [ g o g' ] o equalizer f' g' ] ]
|
|
|
29 uniqueness : {c d : Obj A} (f' : Hom A c a) (g' : Hom A d a) ( e : Hom A c d ) →
|
|
|
30 A [ A [ f o f' ] ≈ A [ A [ g o g' ] o e ] ] → A [ e ≈ equalizer f' g' ]
|
