Mercurial > hg > Members > kono > Proof > category

changeset 1022:2f7e4ad86fc6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Mar 2021 21:21:24 +0900
parents 8a78ddfdaa24
children 227e1fe321ea
files src/CCCSets.agda
diffstat 1 files changed, 60 insertions(+), 30 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Sat Mar 27 13:17:37 2021 +0900
+++ b/src/CCCSets.agda	Sat Mar 27 21:21:24 2021 +0900
@@ -109,9 +109,6 @@
 open import Relation.Nullary
 open import Data.Empty
 
--- data sequ {c : Level} (A B : Set c) ( f g : A → B ) :  Set c where
---     elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g
-
 data Bool { c : Level } : Set c where
      true : Bool
      false : Bool
@@ -125,7 +122,7 @@
      cb : b 
      cl : (y : a) → m cb ≡ y
 
-data _∨_ {c : Level } (a b : Set c) : Set c where
+data _∨_ {c c' : Level } (a : Set c) (b : Set c') : Set (c ⊔ c') where
     case1 : a → a ∨ b
     case2 : b → a ∨ b
 
@@ -138,10 +135,20 @@
 ... | case1 x = record { choice = λ y → x }
 ... | case2 x = record { choice = λ y → ⊥-elim (y x ) }
 
-topos : {c : Level } → ( (b : Set c) → b ∨ (¬ b)) → Topos (Sets {c}) sets
+record Subset {c : Level } {a b : Set c} (m : Hom Sets b a) (y : a) : Set (suc c) where
+   field
+      sb : b
+      isSubset : y ≡ m sb
+
+open import equalizer
+
+Cl : {c : Level } → Set c
+Cl {c} = One {c} ∨ ⊥
+
+topos : {c : Level } → ({ c : Level} →  (b : Set c) → b ∨ (¬ b)) → Topos (Sets {c}) sets
 topos {c} lem = record {
-         Ω = CL {c}
-      ;  ⊤ = λ _ → c1 !
+         Ω = Cl {c}
+      ;  ⊤ = λ _ → case1 !
       ;  Ker = tker
       ;  char = λ m mono → tchar m mono
       ;  isTopos = record {
@@ -149,36 +156,59 @@
               ;  ker-m =  imequ
          }
     } where
-        tker   : {a : Obj Sets} (h : Hom Sets a CL) → Equalizer Sets h (Sets [ (λ _ → c1 !) o CCC.○ sets a ])
+-- data sequ {c : Level} (A B : Set c) ( f g : A → B ) :  Set c where
+--     elem : (x : A ) → (eq : f x ≡ g x) → sequ A B f g
+--
+        data char {c : Level} {a b : Set c} (m : Hom Sets b a) : a → Cl {c} →  Set c where
+          isChar : (x : b ) → char m (m x) (case1 !)
+-- char is function i.e.  y ≡ y' ! → char y ! ≡ char y' !
+        fchar : {a b : Obj (Sets {c})} (m : Hom Sets b a) → (mono : Mono Sets m ) → (y : a ) →  One {c} ∨ ((x : b) → ¬ (m x ≡ y)  )
+        fchar {a} {b} m mono y with lem (char m y (case1 !))
+        ... | case1 (isChar x) = case1 !
+        ... | case2 n = case2 fc1 where
+            fc1 : (x : b) → m x ≡ y → ⊥
+            fc1 x refl = n ( isChar x )
+
+--
+--                   i          ○ b
+--   ker (char m)  ----→ b -----------→ 1
+--       |         ←---- |              |
+--       |           j   |m             | ⊤   char m : a → Ω = {1,⊥}
+--       |   e           ↓    char m    ↓     if y : a ≡ m (∃ x : b) → 1
+--       +-------------→ a -----------→ Ω     else         ⊥
+--                             h
+--
+--     m o i o j ≈ m o id → i o j ≈ id    from mono
+--     j o i ≈ id                         uniqueness of k of ker (char m)
+--     char m o m ≈ (⊤ o  ○ a) o m → e o j ≈ m -- j is k of ker (char m)
+--     char m o e ≈ (⊤ o  ○ a) o e 
+
+        tker   : {a : Obj Sets} (h : Hom Sets a Cl) → Equalizer Sets h (Sets [ (λ _ → case1 !) o CCC.○ sets a ])
         tker {a} h = record {
-                equalizer-c =  sequ a CL h (λ _ → c1 ! )
+                equalizer-c =  sequ a Cl h (λ _ → case1 ! )
               ; equalizer = λ e → equ e
               ; isEqualizer = SetsIsEqualizer _ _ _ _ }
-        tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → CL {c}
-        tchar {a} {b} m mono x = c1 !
-        selem : {a : Obj (Sets {c})} → (x : sequ a CL (λ x₁ → c1 !) (λ _ → c1 ! )) → a
+        tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Cl {c}
+        tchar {a} {b} m mono x = case1 !
+        selem : {a : Obj (Sets {c})} → (x : sequ a Cl (λ x₁ → case1 !) (λ _ → case1 ! )) → a
         selem (elem x eq) = x
-        k-tker : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  → Hom Sets b (b /\ sequ a CL (tchar m mono) (λ _ → c1 ! ))
+        k-tker : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  → Hom Sets b (b /\ sequ a Cl (tchar m mono) (λ _ → case1 ! ))
         k-tker {a} {b} m mono x = record { fst = x ; snd = elem (m x) refl }
-        kr : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  → Hom Sets (b /\ sequ a CL (tchar m mono) (λ _ → c1 ! )) b
+        kr : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  → Hom Sets (b /\ sequ a Cl (tchar m mono) (λ _ → case1 ! )) b
         kr {a} {b} m mono = proj₁
-        imequ   : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → c1 ! ) o CCC.○ sets a ])
-        imequ {a} {b} m mono with lem b
-        ... | case2 n =  record {
-             fe=ge = extensionality Sets ( λ x → refl )
-           ; k = λ h eq y → ?
-           ; ek=h = {!!} 
-           ; uniqueness = {!!} 
-          } 
-        ... | case1 x =  record {
-             fe=ge = extensionality Sets ( λ x → refl )
-           ; k = λ h eq y → proj₁ (k-tker m mono x )
-           ; ek=h = {!!} 
-           ; uniqueness = {!!} 
-          } 
-        uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a CL) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → c1 ! ≡ h x
+        sl : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  → Hom Sets (sequ a Cl (tchar m mono) (λ _ → case1 ! )) (b /\ sequ a Cl (tchar m mono) (λ _ → case1 ! ))
+        sl m mono x = record { fst = {!!} ; snd = x }
+        sr : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  → Hom Sets (b /\ sequ a Cl (tchar m mono) (λ _ → case1 ! )) (sequ a Cl (tchar m mono) (λ _ → case1 ! )) 
+        sr m mono = proj₂
+        isol : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → IsoL Sets m (λ (e : sequ a Cl (tchar m mono)  (λ _ → case1 ! )) → equ e )
+        isol {a} {b} m mono with lem b
+        ... | case1 x = record { iso-L = record { ≅→ = λ _ → elem (m x) refl ; ≅← = λ _ → x ; iso→  = {!!} ; iso←  = {!!} } ; iso≈L = {!!} }
+        ... | case2 n = record { iso-L = record { ≅→ = λ x → ⊥-elim (n x) ; ≅← = λ s → {!!} ; iso→  = {!!} ; iso←  = {!!} } ; iso≈L = {!!} }
+        imequ   : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → case1 ! ) o CCC.○ sets a ])
+        imequ {a} {b} m mono = equalizerIso _ _ (tker (tchar m mono)) m (isol m mono)
+        uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Cl) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → case1 ! ≡ h x
         uniq {a} {b} h m mono x with h x 
-        ... |  c1 ! = refl
+        ... |  case1 ! = refl
            
 
 open import graph