Mercurial > hg > Members > kono > Proof > category
changeset 681:bd8f7346f252
fix Product and pullback
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Nov 2017 17:12:08 +0900 |
| parents | 5d894993477f |
| children | 50a01df1169a |
| files | SetsCompleteness.agda cat-utility.agda pullback.agda |
| diffstat | 3 files changed, 71 insertions(+), 58 deletions(-) [+] |
line wrap: on
line diff
--- a/SetsCompleteness.agda Mon Nov 06 10:10:55 2017 +0900 +++ b/SetsCompleteness.agda Tue Nov 07 17:12:08 2017 +0900 @@ -26,12 +26,12 @@ open Σ public -SetsProduct : { c₂ : Level} → Product ( Sets { c₂} ) -SetsProduct { c₂ } = record { - product = λ a b → Σ a b - ; π1 = λ a b → λ ab → (proj₁ ab) - ; π2 = λ a b → λ ab → (proj₂ ab) - ; isProduct = λ a b → record { +SetsProduct : { c₂ : Level} → ( a b : Obj (Sets {c₂})) → Product ( Sets { c₂} ) a b +SetsProduct { c₂ } a b = record { + product = Σ a b + ; π1 = λ ab → (proj₁ ab) + ; π2 = λ ab → (proj₂ ab) + ; isProduct = record { _×_ = λ f g x → record { proj₁ = f x ; proj₂ = g x } -- ( f x , g x ) ; π1fxg=f = refl ; π2fxg=g = refl
--- a/cat-utility.agda Mon Nov 06 10:10:55 2017 +0900 +++ b/cat-utility.agda Tue Nov 07 17:12:08 2017 +0900 @@ -208,13 +208,13 @@ uniqueness : {c : Obj A} { h : Hom A c ab } → A [ ( A [ π1 o h ] ) × ( A [ π2 o h ] ) ≈ h ] ×-cong : {c : Obj A} { f f' : Hom A c a } → { g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ f × g ≈ f' × g' ] - record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) + record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( a b : Obj A ) : Set (ℓ ⊔ (c₁ ⊔ c₂)) where field - product : (a b : Obj A) → Obj A - π1 : (a b : Obj A) → Hom A (product a b ) a - π2 : (a b : Obj A) → Hom A (product a b ) b - isProduct : (a b : Obj A) → IsProduct A a b (product a b) (π1 a b ) (π2 a b) + product : Obj A + π1 : Hom A product a + π2 : Hom A product b + isProduct : IsProduct A a b product π1 π2 ----- -- @@ -267,27 +267,30 @@ -- | -- d -- - record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b c ab : Obj A) + record IsPullback { 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 + pullback : { 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' ] + → A [ A [ π1 o pullback 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' ] + → A [ A [ π2 o pullback 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 - pi1 : Hom A ab a - pi1 = π1 - pi2 : Hom A ab b - pi2 = π2 + → A [ pullback eq ≈ p' ] + + record Pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b c : Obj A} + ( f : Hom A a c ) ( g : Hom A b c ) + : Set (ℓ ⊔ (c₁ ⊔ c₂)) where + field + ab : Obj A + π1 : Hom A ab a + π2 : Hom A ab b + isPullback : IsPullback A f g π1 π2 -- -- Limit
--- a/pullback.agda Mon Nov 06 10:10:55 2017 +0900 +++ b/pullback.agda Tue Nov 07 17:12:08 2017 +0900 @@ -30,31 +30,41 @@ open IsEqualizer open IsProduct -pullback-from : (a b c ab d : Obj A) +-- ( A [ π1 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) +-- ( A [ π2 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) + +pullback-from : {a b c : Obj A} ( f : Hom A a c ) ( g : Hom A b c ) - ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab ) - ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → IsEqualizer A e f g ) - ( prod : IsProduct A a b ab π1 π2 ) → Pullback A a b c d f g - ( A [ π1 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) - ( A [ π2 o equalizer1 ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ) ] ) -pullback-from a b c ab d f g π1 π2 e eqa prod = record { + ( eqa : {a b : Obj A} → (f g : Hom A a b) → Equalizer A f g ) + ( prod : ( a b : Obj A ) → Product A a b ) → Pullback A f g +pullback-from {a} {b} {c} f g eqa prod0 = record { + ab = ab ; + π1 = A [ π1 o e ] ; + π2 = A [ π2 o e ] ; + isPullback = record { commute = commute1 ; - p = p1 ; + pullback = p1 ; π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ; π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ; uniqueness = uniqueness1 + } } where - commute1 : A [ A [ f o A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] - ≈ A [ g o A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ] + π1 = Product.π1 (prod0 a b ) + π2 = Product.π2 (prod0 a b ) + e = equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) + ab = equalizer-c (eqa (A [ f o π1 ]) (A [ g o π2 ])) + prod = Product.isProduct (prod0 a b) + commute1 : A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] + ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ] commute1 = let open ≈-Reasoning (A) in begin - f o ( π1 o equalizer1 (eqa ( f o π1 ) ( g o π2 )) ) + f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) ≈⟨ assoc ⟩ - ( f o π1 ) o equalizer1 (eqa ( f o π1 ) ( g o π2 )) - ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩ - ( g o π2 ) o equalizer1 (eqa ( f o π1 ) ( g o π2 )) + ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) + ≈⟨ fe=ge (isEqualizer (eqa (A [ f o π1 ]) (A [ g o π2 ]))) ⟩ + ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) ≈↑⟨ assoc ⟩ - g o ( π2 o equalizer1 (eqa ( f o π1 ) ( g o π2 )) ) + g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) ∎ lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ] @@ -72,56 +82,56 @@ ≈⟨ assoc ⟩ ( g o π2 ) o (prod × π1') π2' ∎ - 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' d + 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 = - let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq ) + let open ≈-Reasoning (A) in k (isEqualizer (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ))) (_×_ prod π1' π2' ) ( lemma1 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 [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ] + A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ] o p1 eq ] ≈ π1' ] π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in begin - ( π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq + ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ) o p1 eq ≈⟨⟩ - ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) + ( π1 o e) o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) ≈↑⟨ assoc ⟩ - π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) - ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ + π1 o ( e o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) ) + ≈⟨ cdr ( ek=h (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ))) ⟩ π1 o (_×_ prod π1' π2' ) ≈⟨ π1fxg=f prod ⟩ π1' ∎ π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 [ A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ] + A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ] o p1 eq ] ≈ π2' ] π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in begin - ( π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq + ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) ) ) o p1 eq ≈⟨⟩ - ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) + ( π2 o e) o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) ≈↑⟨ assoc ⟩ - π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) - ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ + π2 o ( e o k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) ) + ≈⟨ cdr ( ek=h (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) ))) ⟩ π2 o (_×_ prod π1' π2' ) ≈⟨ π2fxg=g prod ⟩ π2' ∎ - uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} + 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' ] ]} → - {eq1 : A [ A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → - {eq2 : A [ A [ A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} → + {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → + {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} → A [ p1 eq ≈ p' ] uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in begin p1 eq ≈⟨⟩ - k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) - ≈⟨ IsEqualizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin + k (isEqualizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) (_×_ prod π1' π2' ) (lemma1 eq) + ≈⟨ IsEqualizer.uniqueness (isEqualizer (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) )) ( begin e o p' ≈⟨⟩ - equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' + equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' ≈↑⟨ IsProduct.uniqueness prod ⟩ - (prod × ( π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p')) + (prod × ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p')) ≈⟨ ×-cong prod (assoc) (assoc) ⟩ - (prod × (A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) - (A [ A [ π2 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) + (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) + (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) ≈⟨ ×-cong prod eq1 eq2 ⟩ ((prod × π1') π2') ∎ ) ⟩