Mercurial > hg > Members > kono > Proof > category
comparison equalizer.agda @ 260:a87d3ea9efe4
pullback
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 20 Sep 2013 15:39:50 +0900 |
| parents | c442322d22b3 |
| children | d6a6dd305da2 |
comparison
equal
deleted
inserted
replaced
| 259:c442322d22b3 | 260:a87d3ea9efe4 |
|---|---|
| 18 module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where | 18 module equalizer { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where |
| 19 | 19 |
| 20 open import HomReasoning | 20 open import HomReasoning |
| 21 open import cat-utility | 21 open import cat-utility |
| 22 | 22 |
| 23 record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where | 23 -- in cat-utility |
| 24 field | 24 -- record Equalizer { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {c a b : Obj A} (e : Hom A c a) (f g : Hom A a b) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where |
| 25 fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] | 25 -- field |
| 26 k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c | 26 -- fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] |
| 27 ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] | 27 -- k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c |
| 28 uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → | 28 -- ek=h : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → A [ A [ e o k {d} h eq ] ≈ h ] |
| 29 A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] | 29 -- uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → |
| 30 equalizer : Hom A c a | 30 -- A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] |
| 31 equalizer = e | 31 -- equalizer : Hom A c a |
| 32 -- equalizer = e | |
| 32 | 33 |
| 33 | 34 |
| 34 -- | 35 -- |
| 35 -- Burroni's Flat Equational Definition of Equalizer | 36 -- Burroni's Flat Equational Definition of Equalizer |
| 36 -- | 37 -- |