|
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
|
|
206
|
24 record Equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
|
|
205
|
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' ]
|
|
206
|
31
|
|
|
32 record EqEqualizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A} (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where
|
|
|
33 field
|
|
|
34 α : {d a b : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → Hom A d a
|
|
|
35 γ : {d c : Obj A} → (f : Hom A c b) → (g : Hom A c b ) → (h : Hom A d c ) → Hom A d c
|
|
|
36 δ : {a b : Obj A} → (f : Hom A a b) → Hom A a a
|
|
|
37 β : {c a b d : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A c d ) → Hom A c a
|
|
|
38 b1 : {c : Obj A} → A [ A [ f o α {c} f g ] ≈ A [ g o α {c} f g ] ]
|
|
|
39 b2 : {c d : Obj A } → {h : Hom A d a } → A [ A [ α f g o γ f g h ] ≈ A [ h o α (A [ f o h ]) (A [ g o h ]) ] ]
|
|
|
40 b3 : A [ A [ α f f o δ f ] ≈ id1 A a ]
|
|
|
41 b4 : {c d : Obj A } {k : Hom A c a} → A [ β f g ( A [ α f g o k ] ) ≈ k ]
|
|
|
42 b5 : {c d : Obj A } → {h : Hom A d a } → A [ β f g h ≈ A [ γ f g h o δ (A [ f o h ]) ] ]
|
