Mercurial > hg > Members > kono > Proof > category

changeset 1023:227e1fe321ea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
using Bool and LEM
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Mar 2021 22:52:43 +0900
parents 2f7e4ad86fc6
children 447bbacacf64
files src/CCCSets.agda
diffstat 1 files changed, 35 insertions(+), 76 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Sat Mar 27 21:21:24 2021 +0900
+++ b/src/CCCSets.agda	Sat Mar 27 22:52:43 2021 +0900
@@ -98,57 +98,28 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
---                 ○ b
---   r ←---→ b -----------→ 1
---           |              |
---         m |              | ⊤
---           ↓    char m    ↓
---           a -----------→ Ω
---                 h
-
 open import Relation.Nullary
 open import Data.Empty
+open import equalizer
 
 data Bool { c : Level } : Set c where
      true : Bool
      false : Bool
+
+¬f≡t  : { c : Level } → ¬ (false {c} ≡ true )
+¬f≡t ()
      
-data CL  {c : Level } : Set c where
-     c1 : One {c} → CL
-     φ :  ⊥ → CL
-
-record Char {c : Level } {a b : Obj (Sets {c})} (m : Hom Sets b a) (mono : Mono Sets m) : Set c where
-   field
-     cb : b 
-     cl : (y : a) → m cb ≡ y
-
 data _∨_ {c c' : Level } (a : Set c) (b : Set c') : Set (c ⊔ 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 ) }
-
-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} ∨ ⊥
+data char {c : Level} {a b : Set c} (m : Hom Sets b a) : a → Set c where
+   isChar : (x : b ) → char m (m x) 
 
 topos : {c : Level } → ({ c : Level} →  (b : Set c) → b ∨ (¬ b)) → Topos (Sets {c}) sets
 topos {c} lem = record {
-         Ω = Cl {c}
-      ;  ⊤ = λ _ → case1 !
+         Ω =  Bool
+      ;  ⊤ = λ _ → true
       ;  Ker = tker
       ;  char = λ m mono → tchar m mono
       ;  isTopos = record {
@@ -156,20 +127,9 @@
               ;  ker-m =  imequ
          }
     } where
+--
 -- 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
 --       |         ←---- |              |
@@ -178,37 +138,36 @@
 --       +-------------→ 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 : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true ) o CCC.○ sets a ])
         tker {a} h = record {
-                equalizer-c =  sequ a Cl h (λ _ → case1 ! )
+                equalizer-c =  sequ a Bool h (λ _ → true )
               ; 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 = 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) (λ _ → 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) (λ _ → case1 ! )) b
-        kr {a} {b} m mono = proj₁
-        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 ])
+        tchar : {a b : Obj Sets} (m : Hom Sets b a) → (mono : Mono Sets m ) → a → Bool {c}
+        tchar {a} {b} m mono y with lem (char m y )
+        ... | case1 t = true
+        ... | case2 f = false
+        isol : {a b : Obj (Sets {c}) } (m : Hom Sets b a) → (mono : Mono Sets m ) → IsoL Sets m (λ (e : sequ a Bool (tchar m mono)  (λ _ → true )) → equ e )
+        isol {a} {b} m mono  = record { iso-L = record { ≅→ = b→s ; ≅← = b←s ; iso→  = {!!} ; iso←  = {!!} } ; iso≈L = {!!} } where
+          b→s : Hom Sets b (sequ a Bool (tchar m mono) (λ _ → true))
+          b→s x with lem (char m (m x) )
+          ... | case1 x₁ = bs1 x₁ refl where
+             bs1 : {y : a } → char m y → y ≡ m x  → sequ a Bool (λ y → tchar m mono y) (λ _ → true)
+             bs1 (isChar x) eq = elem (m x) {!!}
+          ... | case2 n = ⊥-elim (n (isChar x))
+          b←s : Hom Sets (sequ a Bool (tchar m mono) (λ _ → true)) b
+          b←s (elem y eq) with lem (char m y)
+          ... | case1 (isChar x) = x
+          ... | case2 t = ⊥-elim ( ¬f≡t eq )
+        imequ   : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsEqualizer Sets m (tchar m mono) (Sets [ (λ _ → true ) 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 
-        ... |  case1 ! = refl
+        uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (y : a) →
+               tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) }) y ≡ h y
+        uniq {a} {b} h m mono y with h y  | lem (char (Equalizer.equalizer (tker h)) y ) | inspect (tchar (Equalizer.equalizer (tker h)) (record { isMono = λ f g → monic (tker h) })) y
+        ... | true | case1 x | record { eq = eq1 } = eq1 
+        ... | true | case2 x | record { eq = eq1 } = {!!}
+        ... | false | case1 x | record { eq = eq1 }  = {!!}
+        ... | false | case2 x | record { eq = eq1 }  = eq1
            
 
 open import graph