Mercurial > hg > Members > kono > Proof > category
changeset 672:749df4959d19
fix completeness
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 02 Nov 2017 09:00:01 +0900 |
| parents | 959954fc29f8 |
| children | 0007f9a25e9c |
| files | S.agda SetsCompleteness.agda cat-utility.agda freyd.agda pullback.agda |
| diffstat | 5 files changed, 35 insertions(+), 35 deletions(-) [+] |
line wrap: on
line diff
--- a/S.agda Mon Oct 30 18:18:36 2017 +0900 +++ b/S.agda Thu Nov 02 09:00:01 2017 +0900 @@ -26,12 +26,12 @@ open snat - snat-cong' : { c : Level } { I OC : Set c } { SObj : OC → Set c } { SMap : { i j : OC } → (f : I )→ SObj i → SObj j } - ( s t : snat SObj SMap ) - → ( ( λ i → snmap s i ) ≡ ( λ i → snmap t i ) ) - → ( ( λ i j f → smap0 s f ( snmap s i ) ≡ snmap s j ) ≡ ( ( λ i j f → smap0 t f ( snmap t i ) ≡ snmap t j ) ) ) - → s ≡ t - snat-cong' s t refl refl = {!!} + -- snat-cong' : { c : Level } { I OC : Set c } { SObj : OC → Set c } { SMap : { i j : OC } → (f : I )→ SObj i → SObj j } + -- ( s t : snat SObj SMap ) + -- → ( ( λ i → snmap s i ) ≡ ( λ i → snmap t i ) ) + -- → ( ( λ i j f → smap0 s f ( snmap s i ) ≡ snmap s j ) ≡ ( ( λ i j f → smap0 t f ( snmap t i ) ≡ snmap t j ) ) ) + -- → s ≡ t + -- snat-cong' s t refl refl = {!!} snat-cong : {c : Level} {I OC : Set c}
--- a/SetsCompleteness.agda Mon Oct 30 18:18:36 2017 +0900 +++ b/SetsCompleteness.agda Thu Nov 02 09:00:01 2017 +0900 @@ -26,7 +26,7 @@ open Σ public -SetsProduct : { c₂ : Level} → CreateProduct ( Sets { c₂} ) +SetsProduct : { c₂ : Level} → Product ( Sets { c₂} ) SetsProduct { c₂ } = record { product = λ a b → Σ a b ; π1 = λ a b → λ ab → (proj₁ ab) @@ -274,11 +274,13 @@ open Limit open IsLimit +open IProduct SetsCompleteness : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( small : Small C I ) → Complete (Sets {c₁}) C SetsCompleteness {c₁} {c₂} C I s = record { climit = λ Γ → SetsLimit {c₁} C I s Γ - ; equalizer-p = λ {a} {b} f g → sequ a b f g - ; equalizer-e = λ {a} {b} f g → ( λ e → equ e ) - ; isEqualizer = λ {a} {b} f g → SetsIsEqualizer a b f g + ; cequalizer = λ {a} {b} f g → record { equalizer-c = sequ a b f g ; + equalizer = ( λ e → equ e ) ; + isEqualizer = SetsIsEqualizer a b f g } + ; cproduct = λ J fi → SetsIProduct J fi } where
--- a/cat-utility.agda Mon Oct 30 18:18:36 2017 +0900 +++ b/cat-utility.agda Thu Nov 02 09:00:01 2017 +0900 @@ -197,7 +197,7 @@ -- π1 π2 - record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (a b ab : Obj A) + record IsProduct { 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 @@ -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 CreateProduct { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) + record Product { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) : 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) -> Product A a b (product a b) (π1 a b ) (π2 a b) + 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) ----- -- @@ -356,26 +356,24 @@ record CreateLimit { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where field - climit : ( Γ : Functor I A ) -> Limit A I Γ + climit : ( Γ : Functor I A ) → Limit A I Γ record Complete { c₁' c₂' ℓ' : Level} { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( I : Category c₁' c₂' ℓ' ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where field - climit : ( Γ : Functor I A ) -> Limit A I Γ - - -- 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) -> Product A a b (product a b) (π1 a b ) (π2 a b) - - equalizer-p : {a b : Obj A} (f g : Hom A a b) -> Obj A - equalizer-e : {a b : Obj A} (f g : Hom A a b) -> Hom A (equalizer-p f g) a - isEqualizer : {a b : Obj A} (f g : Hom A a b) -> IsEqualizer A (equalizer-e f g) f g + climit : ( Γ : Functor I A ) → Limit A I Γ + cproduct : ( I : Set c₁' ) (fi : I → Obj A ) → IProduct A I -- c₁ should be a free level + cequalizer : {a b : Obj A} (f g : Hom A a b) → Equalizer A f g open Limit - limit-c : ( Γ : Functor I A ) -> Obj A + limit-c : ( Γ : Functor I A ) → Obj A limit-c Γ = a0 ( climit Γ) - limit-u : ( Γ : Functor I A ) -> NTrans I A ( K A I (limit-c Γ )) Γ + limit-u : ( Γ : Functor I A ) → NTrans I A ( K A I (limit-c Γ )) Γ limit-u Γ = t0 ( climit Γ) + open Equalizer + equalizer-p : {a b : Obj A} (f g : Hom A a b) → Obj A + equalizer-p f g = equalizer-c (cequalizer f g ) + equalizer-e : {a b : Obj A} (f g : Hom A a b) → Hom A (equalizer-p f g) a + equalizer-e f g = equalizer (cequalizer f g ) -- initial object
--- a/freyd.agda Mon Oct 30 18:18:36 2017 +0900 +++ b/freyd.agda Thu Nov 02 09:00:01 2017 +0900 @@ -66,7 +66,7 @@ u : NTrans A A (K A A a00) F u = t0 ( lim F ) equ : {a b : Obj A} → (f g : Hom A a b) → IsEqualizer A (equalizer-e comp f g ) f g - equ f g = Complete.isEqualizer comp f g + equ f g = isEqualizer ( Complete.cequalizer comp f g ) ep : {a b : Obj A} → {f g : Hom A a b} → Obj A ep {a} {b} {f} {g} = equalizer-p comp f g ee : {a b : Obj A} → {f g : Hom A a b} → Hom A (ep {a} {b} {f} {g} ) a
--- a/pullback.agda Mon Oct 30 18:18:36 2017 +0900 +++ b/pullback.agda Thu Nov 02 09:00:01 2017 +0900 @@ -28,14 +28,14 @@ open Equalizer open IsEqualizer -open Product +open IsProduct open Pullback pullback-from : (a b c ab d : 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 : Product A a b ab π1 π2 ) → Pullback A a b c d 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 { @@ -118,7 +118,7 @@ e o p' ≈⟨⟩ equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' - ≈↑⟨ Product.uniqueness prod ⟩ + ≈↑⟨ 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')) ≈⟨ ×-cong prod (assoc) (assoc) ⟩ (prod × (A [ A [ π1 o equalizer1 (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) @@ -289,13 +289,13 @@ ∎ -lemma-p0 : (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : Product A a b ab π1 π2 ) → +lemma-p0 : (a b ab : Obj A) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( prod : IsProduct A a b ab π1 π2 ) → A [ _×_ prod π1 π2 ≈ id1 A ab ] lemma-p0 a b ab π1 π2 prod = let open ≈-Reasoning (A) in begin _×_ prod π1 π2 ≈↑⟨ ×-cong prod idR idR ⟩ _×_ prod (A [ π1 o id1 A ab ]) (A [ π2 o id1 A ab ]) - ≈⟨ Product.uniqueness prod ⟩ + ≈⟨ IsProduct.uniqueness prod ⟩ id1 A ab ∎