Mercurial > hg > Members > kono > Proof > category

comparison equalizer.agda @ 205:242adb6669da

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalizer
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 01 Sep 2013 22:10:39 +0900
parents
children 3a5e2a22e053
comparison
equal deleted inserted replaced
204:b2874c5086ea 205:242adb6669da
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' ]