Mercurial > hg > Members > kono > Proof > category

changeset 669:220ea177572f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix completeness
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Oct 2017 17:49:58 +0900
parents 07c84c8d9e4f
children 99065a1e56ea
files SetsCompleteness.agda cat-utility.agda
diffstat 2 files changed, 22 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Oct 30 11:57:49 2017 +0900
+++ b/SetsCompleteness.agda	Mon Oct 30 17:49:58 2017 +0900
@@ -112,7 +112,7 @@
 --           equalizer-c = sequ a b f g
 --          ; equalizer = λ e → equ e
 
-SetsIsEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e )f g
+SetsIsEqualizer :  {  c₂ : Level}  →  (a b : Obj (Sets {c₂}) )  (f g : Hom (Sets {c₂}) a b) → IsEqualizer Sets (λ e → equ e) f g
 SetsIsEqualizer {c₂} a b f g = record {
                fe=ge  = fe=ge
              ; k = k
@@ -170,20 +170,15 @@
    field
        snmap : ( i : OC ) → sobj i
        sncommute : ( i j : OC ) → ( f :  I ) →  smap f ( snmap i )  ≡ snmap j
-   smap0 :  { i j :  OC  }  → (f : I ) →  sobj i → sobj j
-   smap0 {i} {j} f x =  smap f x
 
 open snat
 
-≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C )
-    →  a  ≡  a'
-    →  b  ≡  b'
-    →  f a b  ≡  f a' b'
-≡cong2 _ refl refl = refl
-
 open import Relation.Binary.HeterogeneousEquality as HE renaming ( cong to cong' ; sym to sym' ; subst₂ to subst₂' ; Extensionality to Extensionality' )
     using (_≅_;refl; ≡-to-≅)
-postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → HE.Extensionality c₂ c₂
+-- why we cannot use Extensionality' ?
+postulate ≅extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → 
+                  {a : Level } {A : Set a} {B B' : A → Set a}
+                               {f : (y : A) → B y} {g : (y : A) → B' y} → (∀ y → f y ≅ g y) → ( ( λ y → f y ) ≅ ( λ y → g y ))
 
 snat-cong : {c : Level}
                 {I OC : Set c}
@@ -222,7 +217,7 @@
 
 SetsLimit : {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ ) ( small : Small C I ) ( Γ : Functor C (Sets  {c₁} ) )
     → Limit Sets C Γ
-SetsLimit { c₂} C I s Γ = record {
+SetsLimit {c₁} C I s Γ = record {
            a0 =  snat  (ΓObj s Γ) (ΓMap s Γ)
          ; t0 = Cone C I s Γ
          ; isLimit = record {
@@ -260,20 +255,30 @@
                   open ≡-Reasoning
                   eq1 : (x : a ) (i : Obj C) → TMap t i x ≡ snmap (f x) i
                   eq1 x i = sym ( ≡cong ( λ f → f x ) cif=t  )
-                  eq2 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (TMap t i x) ≡ TMap t j x -- hg cat -r 550 SetsCompleteness.agda
+                  eq2 : (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (TMap t i x) ≡ TMap t j x 
                   eq2 x i j f =  ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
                   eq3 :  (x : a ) (i j : Obj C) (k : I) → ΓMap s Γ k (snmap (f x) i) ≡ snmap (f x) j
                   eq3 x i j k =  sncommute (f x ) i j k
                   irr≅ : { c₂ : Level}  {d e : Set c₂ }  { x1 y1 : d } { x2 y2 : e }
-                      ( ee :  x1 ≅ x2 ) ( ee :  y1  ≅ y2 )  ( eq :  x1  ≡ y1 ) ( eq' :  x2  ≡ y2 ) → eq ≅ eq'
+                      ( ee :  x1 ≅ x2 ) ( ee' :  y1  ≅ y2 )  ( eq :  x1  ≡ y1 ) ( eq' :  x2  ≡ y2 ) → eq ≅ eq'
                   irr≅ refl refl refl refl = refl
                   eq4 :  ( x : a)  ( i j : Obj C ) ( g : I )
                      → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g }  ) ≅  sncommute (f x) i j g
                   eq4 x i j g = irr≅ (≡-to-≅ (≡cong ( λ h → ΓMap s Γ g h ) (eq1 x i))) (≡-to-≅ (eq1 x j )) (eq2 x i j g ) (eq3 x i j g )
-                  -- heterogenous extensionarity
-                  postulate eq6 : {a : Level } {A : Set a} {B B' : A → Set a}
-                               {f : (y : A) → B y} {g : (y : A) → B' y} → (∀ y → f y ≅ g y) → ( ( λ y → f y ) ≅ ( λ y → g y ))
                   eq5 :  ( x : a) 
                       →  ( λ i j g → ≡cong ( λ h → h x ) ( IsNTrans.commute ( isNTrans t ) {i} {j} {hom← s g } ))
                        ≅ ( λ i j g →  sncommute (f x) i j g )
-                  eq5 x = eq6 ( λ i → eq6 ( λ j → eq6 ( λ g → eq4 x i j g ) ) )
+                  eq5 x = ≅extensionality (Sets {c₁} ) ( λ i →
+                          ≅extensionality (Sets {c₁} ) ( λ j →
+                          ≅extensionality (Sets {c₁} ) ( λ g → eq4 x i j g ) ) )
+
+open Limit
+open IsLimit
+
+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 
+   } where
--- a/cat-utility.agda	Mon Oct 30 11:57:49 2017 +0900
+++ b/cat-utility.agda	Mon Oct 30 17:49:58 2017 +0900
@@ -362,7 +362,6 @@
                 : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where
           field
              climit :  ( Γ : Functor I A ) -> Limit A I Γ 
-             alimit :  ( Γ : Functor I A ) (a0 : Obj A ) ( t0 : NTrans I A ( K A I a0 ) Γ )  -> IsLimit A I Γ a0 t0
 
              -- product : (a b : Obj A) -> Obj A
              -- π1 : (a b : Obj A) -> Hom A (product a b ) a