Mercurial > hg > Members > kono > Proof > category

changeset 1021:8a78ddfdaa24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... use LEM for Topos Sets
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Mar 2021 13:17:37 +0900
parents d7e89e26700e
children 2f7e4ad86fc6
files src/CCCSets.agda
diffstat 1 files changed, 26 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Sat Mar 27 08:53:04 2021 +0900
+++ b/src/CCCSets.agda	Sat Mar 27 13:17:37 2021 +0900
@@ -125,8 +125,21 @@
      cb : b 
      cl : (y : a) → m cb ≡ y
 
-topos : {c : Level } → ( {a b : Obj (Sets {c})} (m : Hom Sets b a) (mono : Mono Sets m) → Dec (Char m mono )) → Topos (Sets {c}) sets
-topos {c} dec = record {
+data _∨_ {c : Level } (a b : Set c) : Set c where
+    case1 : a → a ∨ b
+    case2 : b → a ∨ b
+
+record Choice {c : Level } (b : Set c) : Set c where
+   field
+      choice : ¬ (¬ b ) → b
+
+lem2choice : {c : Level } → {b : Set c} →  b ∨ (¬ b) → Choice b
+lem2choice {c} {b} lem with lem
+... | 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
+topos {c} lem = record {
          Ω = CL {c}
       ;  ⊤ = λ _ → c1 !
       ;  Ker = tker
@@ -147,20 +160,19 @@
         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} m mono x = record { fst = x ; snd = elem (m x) refl }
-        bb : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  → Iso Sets b (b /\ sequ a CL (tchar m mono) (λ _ → c1 !))
-        bb {a} {b} m mono = record { ≅→ = λ x →  record { fst = x ; snd = elem (m x) refl } ; ≅← = proj₁ ; iso→  = extensionality Sets ( λ x → refl )
-          ; iso←  = {!!} } where
-             bb1 : (x : b /\ sequ a CL (tchar m mono) (λ _ → c1 !) ) → elem (m (proj₁ x)) refl ≡ proj₂ x
-             bb1 (x , elem y eq) = {!!}
-        ss : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m )  → Iso Sets (b /\ sequ a CL (tchar m mono) (λ _ → c1 !)) (sequ a CL (tchar m mono) (λ _ → c1 !))
-        ss {a} {b} m mono = record { ≅→ = λ x →  elem (m (proj₁ x)) refl ; ≅← = ss1 ; iso→  = extensionality Sets ( λ x → {!!} )
-          ; iso←  = extensionality Sets ( λ x → {!!} ) } where
-             ss1 :  Hom Sets (sequ a CL (tchar m mono) (λ _ → c1 !)) (b /\ sequ a CL (tchar m mono) (λ _ → c1 !))
-             ss1 (elem x eq) = record { fst = {!!} ; snd = elem x eq }
+        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} 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   = record {
+        imequ {a} {b} m mono with lem b
+        ... | case2 n =  record {
              fe=ge = extensionality Sets ( λ x → refl )
-           ; k = {!!} -- λ h eq y → proj₁ (k-tker {!!} {!!} {!!} )
+           ; 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 = {!!} 
           }