Mercurial > hg > Members > kono > Proof > category
comparison src/CCC.agda @ 1034:40c39d3e6a75
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 31 Mar 2021 15:58:02 +0900 |
| parents | 4b517d46e987 |
| children | 849f85e543f1 |
comparison
equal
deleted
inserted
replaced
| 1033:a59c51b541a2 | 1034:40c39d3e6a75 |
|---|---|
| 191 -- | m | | ⊤ | 191 -- | m | | ⊤ |
| 192 -- | ↓ char m ↓ Ker h = Equalizer (char m mono) (⊤ ∙ ○ a ) | 192 -- | ↓ char m ↓ Ker h = Equalizer (char m mono) (⊤ ∙ ○ a ) |
| 193 -- + ------→ a -----------→ Ω m = Equalizer (char m mono) (⊤ ∙ ○ a ) | 193 -- + ------→ a -----------→ Ω m = Equalizer (char m mono) (⊤ ∙ ○ a ) |
| 194 -- ker h h | 194 -- ker h h |
| 195 -- | 195 -- |
| 196 -- if m is an equalizer, there is an iso between e and b as k, and if we have the iso, m becomes an equalizer. | |
| 197 -- equalizer.equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g ) | |
| 198 -- → (m : Hom A c a) → ( ker-iso : IsoL A m (equalizer equ) ) → IsEqualizer A m f g | |
| 199 | |
| 196 open Equalizer | 200 open Equalizer |
| 197 open import equalizer | 201 open import equalizer |
| 198 | 202 |
| 199 record Mono {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set (c₁ ⊔ c₂ ⊔ ℓ) where | 203 record Mono {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set (c₁ ⊔ c₂ ⊔ ℓ) where |
| 200 field | 204 field |