Mercurial > hg > Members > kono > Proof > category

changeset 1020:d7e89e26700e

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 08:53:04 +0900
parents 501e016bf877
children 8a78ddfdaa24
files src/CCCSets.agda
diffstat 1 files changed, 53 insertions(+), 45 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Thu Mar 25 14:23:51 2021 +0900
+++ b/src/CCCSets.agda	Sat Mar 27 08:53:04 2021 +0900
@@ -26,12 +26,12 @@
 -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Axiom.Extensionality.Propositional.Extensionality  c₂ c₂
 
 data One  {c : Level } : Set c where
-  OneObj : One   -- () in Haskell ( or any one object set )
+  ! : One   -- () in Haskell ( or any one object set )
 
 sets : {c : Level } → CCC (Sets {c})
 sets  = record {
          １  = One
-       ; ○ = λ _ → λ _ → OneObj
+       ; ○ = λ _ → λ _ → !
        ; _∧_ = _∧_
        ; <_,_> = <,>
        ; π = π
@@ -44,7 +44,7 @@
          １ : Obj Sets 
          １ = One 
          ○ : (a : Obj Sets ) → Hom Sets a １
-         ○ a = λ _ → OneObj
+         ○ a = λ _ → !
          _∧_ : Obj Sets → Obj Sets → Obj Sets
          _∧_ a b =  a /\  b
          <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b)
@@ -75,7 +75,7 @@
                   where
                         e20 : (x : a ) → f x ≡ ○ a x
                         e20 x with f x
-                        e20 x | OneObj = refl
+                        e20 x | ! = refl
                 e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
                     Sets [ ( Sets [  π  o ( <,> f g)  ] ) ≈ f ]
                 e3a = refl
@@ -98,67 +98,75 @@
                     Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                 *-cong refl = refl
 
---             ○ b
---       b -----------→ 1
---       |              |
---     m |              | ⊤
---       ↓    char m    ↓
---       a -----------→ Ω
---             h
+--                 ○ b
+--   r ←---→ b -----------→ 1
+--           |              |
+--         m |              | ⊤
+--           ↓    char m    ↓
+--           a -----------→ Ω
+--                 h
 
-data Bool  {c : Level } : Set c where
-     true : Bool
-     false : Bool
+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
 
--- irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
--- irr refl refl = refl
-
-open import Relation.Nullary
-open import Data.Empty
+data Bool { c : Level } : Set c where
+     true : Bool
+     false : Bool
+     
+data CL  {c : Level } : Set c where
+     c1 : One {c} → CL
+     φ :  ⊥ → CL
 
-topos : {c : Level } → Topos (Sets {c}) sets
-topos {c}  = record {
-         Ω = Bool
-      ;  ⊤ = λ _ → true
+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
+
+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 {
+         Ω = CL {c}
+      ;  ⊤ = λ _ → c1 !
       ;  Ker = tker
-      ;  char = tchar
+      ;  char = λ m mono → tchar m mono
       ;  isTopos = record {
                  char-uniqueness  = λ {a} {b} {h} m mono →  extensionality Sets ( λ x → uniq h m mono x )
               ;  ker-m =  imequ
          }
     } where
-        tker   : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true) o CCC.○ sets a ])
+        tker   : {a : Obj Sets} (h : Hom Sets a CL) → Equalizer Sets h (Sets [ (λ _ → c1 !) o CCC.○ sets a ])
         tker {a} h = record {
-                equalizer-c =  sequ a Bool h (λ _ → true)
+                equalizer-c =  sequ a CL h (λ _ → c1 ! )
               ; equalizer = λ e → equ e
               ; isEqualizer = SetsIsEqualizer _ _ _ _ }
-        tchar : {a b : Obj Sets} (m : Hom Sets b a) → Mono Sets m → Hom Sets a Bool
-        tchar {a} {b} m mono x = true
-        selem : {a : Obj (Sets {c})} → (x : sequ a Bool (λ x₁ → true) (λ _ → true)) → a
+        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
         selem (elem x eq) = x
-        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 ])
+        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 }
+        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 {
              fe=ge = extensionality Sets ( λ x → refl )
-           ; k = λ h eq → {!!}
+           ; k = {!!} -- λ h eq y → proj₁ (k-tker {!!} {!!} {!!} )
            ; ek=h = {!!} 
            ; uniqueness = {!!} 
           } 
-        uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → true ≡ h x
-        uniq {a} {b} h m mono x with IsEqualizer.fe=ge (Equalizer.isEqualizer (tker h)) | h x | inspect h x
-        ... | t | true | _ = refl
-        ... | t | false | record { eq = eq1 } = ⊥-elim ( uniq1 t ) where
-             neq : _≡_ {c} {Bool} true false → ⊥
-             neq ()
-             se : sequ a Bool h (λ _ → true)
-             se = elem x ? -- Mono.isMono mono ? ? ?  -- Equalizer.equalizer-c (tker h)
-             uniq1 : (λ x₁ → h (equ x₁)) ≡ (λ x₁ → true) → ⊥
-             uniq1 eq = neq ( begin
-                true ≡⟨ cong (λ k → k se) (sym eq)  ⟩
-                h x ≡⟨ eq1 ⟩
-                false ∎ ) where  open ≡-Reasoning 
+        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
+        uniq {a} {b} h m mono x with h x 
+        ... |  c1 ! = refl
            
 
 open import graph
@@ -262,7 +270,7 @@
    amap ε (f , x ) = f x
    amap (f *) x = λ y →  fmap f ( x , y ) 
    fmap (id a) x = x
-   fmap (○ a) x = OneObj
+   fmap (○ a) x = !
    fmap < f , g > x = ( fmap f x , fmap g x )
    fmap (iv x f) a = amap x ( fmap f a )