Mercurial > hg > Members > kono > Proof > category
changeset 260:a87d3ea9efe4
pullback
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 20 Sep 2013 15:39:50 +0900 |
| parents | c442322d22b3 |
| children | a2477147dfec |
| files | cat-utility.agda equalizer.agda pullback.agda |
| diffstat | 3 files changed, 125 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Tue Sep 17 11:27:57 2013 +0900 +++ b/cat-utility.agda Fri Sep 20 15:39:50 2013 +0900 @@ -139,3 +139,65 @@ -- μR=μ : {x : Obj A } -> A [ TMap μR x ≈ TMap μ x ] + 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 + field + fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] + k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c + 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 ] + uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → + A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] + equalizer : Hom A c a + equalizer = e + + -- + -- Product + -- + -- + -- + -- + -- + -- + -- + + + record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) + ( π1 : Hom A ab a ) + ( π2 : Hom A ab b ) + : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + _×_ : {c : Obj A} ( f : Hom A c a ) → ( g : Hom A c b ) → Hom A c ab + π1fxg=f : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π1 o ( f × g ) ] ≈ f ] + π2fxg=g : {c : Obj A} { f : Hom A c a } → { g : Hom A c b } → A [ A [ π2 o ( f × g ) ] ≈ g ] + uniqueness : {c : Obj A} { h : Hom A c ab } → A [ ( A [ π1 o h ] ) × ( A [ π2 o h ] ) ≈ h ] + axb : Obj A + axb = ab + + -- + -- Pullback + -- f + -- a -------> c + -- ^ ^ + -- π1 | |g + -- | | + -- ab -------> b + -- ^ π2 + -- | + -- d + -- + record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b c ab : Obj A) + ( f : Hom A a c ) ( g : Hom A b c ) + ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) + : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + commute : A [ A [ f o π1 ] ≈ A [ g o π2 ] ] + p : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d ab + π1p=π1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → A [ A [ π1 o p eq ] ≈ π1' ] + π2p=π2 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → A [ A [ π2 o p eq ] ≈ π2' ] + uniqueness : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → { π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] } + → { π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] } + → A [ p eq ≈ p' ] + axb : Obj A + axb = ab
--- a/equalizer.agda Tue Sep 17 11:27:57 2013 +0900 +++ b/equalizer.agda Fri Sep 20 15:39:50 2013 +0900 @@ -20,15 +20,16 @@ open import HomReasoning open import cat-utility -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 - field - fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] - k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c - 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 ] - uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → - A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] - equalizer : Hom A c a - equalizer = e +-- in cat-utility +-- 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 +-- field +-- fe=ge : A [ A [ f o e ] ≈ A [ g o e ] ] +-- k : {d : Obj A} (h : Hom A d a) → A [ A [ f o h ] ≈ A [ g o h ] ] → Hom A d c +-- 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 ] +-- uniqueness : {d : Obj A} → ∀ {h : Hom A d a} → {eq : A [ A [ f o h ] ≈ A [ g o h ] ] } → {k' : Hom A d c } → +-- A [ A [ e o k' ] ≈ h ] → A [ k {d} h eq ≈ k' ] +-- equalizer : Hom A c a +-- equalizer = e --
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/pullback.agda Fri Sep 20 15:39:50 2013 +0900 @@ -0,0 +1,53 @@ +-- Pullback from product and equalizer +-- +-- +-- Shinji KONO <kono@ie.u-ryukyu.ac.jp> +---- + +open import Category -- https://github.com/konn/category-agda +open import Level +module pullback { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where + +open import HomReasoning +open import cat-utility + +-- +-- Pullback +-- f +-- a -------> c +-- ^ ^ +-- π1 | |g +-- | | +-- ab -------> b +-- ^ π2 +-- | +-- d +-- + +pullback-from : (a b c ab : Obj A) + ( f : Hom A a c ) ( g : Hom A b c ) + ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) + ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) + ( prod : Product A a b ab π1 π2 ) → Pullback A a b c ab f g π1 π2 +pullback-from a b c ab f g π1 π2 eqa prod = record { + commute = commute1 ; + p = p1 ; + π1p=π1 = π1p=π11 ; + π2p=π2 = π2p=π21 ; + uniqueness = uniqueness1 + } where + commute1 : A [ A [ f o π1 ] ≈ A [ g o π2 ] ] + commute1 = ? + p1 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d ab + p1 {d} { π1' } { π2' } eq = ? + π1p=π11 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → A [ A [ π1 o p1 eq ] ≈ π1' ] + π1p=π11 { d } { π1' } { π2' } { eq } = ? + π2p=π21 : { d : Obj A } → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → A [ A [ π2 o p1 eq ] ≈ π2' ] + π2p=π21 { d } { π1' } { π2' } { eq } = ? + uniqueness1 : { d : Obj A } → ( p' : Hom A d ab ) → { π1' : Hom A d a } { π2' : Hom A d b } → { eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ] } + → { π1p=π1' : A [ A [ π1 o p' ] ≈ π1' ] } + → { π2p=π2' : A [ A [ π2 o p' ] ≈ π2' ] } + → A [ p1 eq ≈ p' ] + uniqueness1 { d } p' { π1' } { π2' } { eq }{ π1p=π1' } { π2p=π2' } = ?