Mercurial > hg > Members > kono > Proof > category

changeset 1038:db3e89065178

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 Wed, 07 Apr 2021 15:17:38 +0900
parents f757156ac9fe
children 572de732853f
files src/ToposEx.agda src/ToposIL.agda src/ToposSub.agda
diffstat 3 files changed, 160 insertions(+), 67 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposEx.agda	Fri Apr 02 19:55:43 2021 +0900
+++ b/src/ToposEx.agda	Wed Apr 07 15:17:38 2021 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 open import CCC
 open import Level
 open import Category
@@ -10,7 +11,7 @@
   open ≈-Reasoning A
   open CCC.CCC c
 
-
+--
 --             ○ b
 --       b -----------→ 1
 --       |              |
@@ -365,12 +366,6 @@
   partialmapClassifier : (b : Obj A) → PartialmapClassifier b
   partialmapClassifier = {!!}
 
-  record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
-     field
-        sb : Obj A
-        sm : Hom A sb a 
-        smono : Mono A sm
-
   postulate
     I : Set c₁
     small : Small A I 
@@ -383,63 +378,3 @@
   toposS : Topos SetsAop cs
   toposS = {!!}
 
--- 
---   module SubObjectFunctor
---      (S : (a : Set (c₁ ⊔ c₂ ⊔ ℓ))  → Set c₂)
---      (solv← : {x : Obj A} → S (SubObject x) → SubObject x)
---      (solv→ : {x : Obj A} → SubObject x → S (SubObject x))
---      (soiso← : {a : Obj A} → (x : SubObject a) → solv← (solv→ x) ≡ x)
---      (soiso→ : {a : Obj A} → (x : S (SubObject a) ) → solv→ (solv← x) ≡ x)
---      (≡←≈ :   {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y) where
--- 
---     open SubObject 
--- 
---     Smap : {x y : Obj A} → Hom A y x → Hom Sets (S (SubObject x)) (S (SubObject y))
---     Smap {x} {y} h s = solv→ record { sb = y ; sm = id1 A y ; smono = record { isMono = λ f g eq → sm1 f g eq } } where
---          sm1 : {a : Obj A } → ( f g : Hom A a y ) → A [ A [ id1 A y o f ]  ≈ A [ id1 A y o g ] ] → A [ f  ≈ g ]
---          sm1 f g eq = begin
---               f ≈↑⟨ idL ⟩ 
---               id1 A y o f ≈⟨ eq ⟩ 
---               id1 A y o g ≈⟨ idL  ⟩ 
---               g ∎  
--- 
---     SubObjectFuntor  : Functor  (Category.op A)  (Sets {c₂})
---     SubObjectFuntor  = record {
---          FObj = λ x → S (SubObject x)
---        ; FMap = Smap
---        ; isFunctor  = record {
---               identity = {!!}
---             ; distr  = {!!}
---             ; ≈-cong  = {!!}
---           }
---        } 
--- 
---     open NTrans 
---     sub→topos : (Ω : Obj A) → Representable A ≡←≈ SubObjectFuntor Ω → Topos A c
---     sub→topos Ω R = record {
---           Ω =  Ω
---        ;  ⊤ = TMap (Representable.repr→ R) １ (solv→ record { sb = {!!} ; sm = {!!} ; smono = {!!} })
---        ;  Ker = λ {a} h → record { equalizer-c = sb {!!}
---           ; equalizer = sm {!!}
---           ; isEqualizer = {!!}
---           }
---        ;  char = λ m mono → {!!} 
---        ;  isTopos = record {
---           char-uniqueness  = {!!}
---        ;  ker-m = {!!}
---           } }
---  
---     topos→rep : (t : Topos A c ) → Representable A ≡←≈ SubObjectFuntor (Topos.Ω t)
---     topos→rep t = record {
---         repr→ = record { TMap = λ a Sa → Topos.char t (sm (solv← Sa)) (smono (solv← Sa)) ; isNTrans = record { commute = {!!} } } -- Hom A a Ω
---       ; repr← = record { TMap = λ a h →  solv→ record {sb = equalizer-c (Ker t h) ; sm = equalizer (Ker t h) ; smono =
---          {!!} } ; isNTrans = {!!} }  -- FObj (Sub S) a
---       ; reprId→  = {!!}
---       ; reprId←  = {!!}
---      }
---  
---  
--- 
--- 
-
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ToposIL.agda	Wed Apr 07 15:17:38 2021 +0900
@@ -0,0 +1,63 @@
+open import CCC
+open import Level
+open import Category
+open import cat-utility
+open import HomReasoning
+open import Data.List hiding ( [_] )
+module ToposIL   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ c)) where
+
+  open Topos
+  open Equalizer
+  open ≈-Reasoning A
+  open CCC.CCC c
+
+  open Functor
+  open import Category.Sets hiding (_o_)
+  open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
+
+  -- record IsLogic    (c : CCC A) 
+  --        (Ω : Obj A)
+  --        (⊤ : Hom A (CCC.１ c) Ω)
+  --        (P  : Obj A → Obj A)
+  --        (_==_ : {a : Obj A} (x y : Hom A  (CCC.１ c) a ) → Hom A ( a ∧ a ) Ω)
+  --        (_∈_ : {a : Obj A} (x : Hom A (CCC.１ c) a ) → Hom A ( a ∧ P a ) Ω)
+  --        (_|-_  : {a : Obj A} (x : List ( Hom A (CCC.１ c) a ) ) → Hom A {!!} Ω)
+  --           :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+  --    field
+  --        a : {!!}
+
+  record Logic    (c : CCC A)  :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+     field
+         Ω : Obj A
+         ⊤ : Hom A (CCC.１ c) Ω
+         P  : Obj A → Obj A
+         _==_ : {a : Obj A} (x y : Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) Ω
+         _∈_ : {a : Obj A} (x :  Hom A  (CCC.１ c) a ) (α : Hom A (CCC.１ c) (P a) ) → Hom A (CCC.１ c) Ω
+         _|-_  : {a : Obj A} (x : List ( Hom A (CCC.１ c) a ) ) → Hom A {!!} Ω
+         -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
+  
+--             ○ b
+--       b -----------→ 1
+--       |              |
+--     m |              | ⊤
+--       ↓    char m    ↓
+--       a -----------→ Ω
+
+  open NatD
+  open ToposNat n
+
+  N : Obj A
+  N = Nat iNat 
+
+  open import ToposEx A c t n using ( δmono  )
+
+  topos→logic : Logic c
+  topos→logic = record {
+         Ω = Topos.Ω t
+      ;  ⊤ = Topos.⊤ t
+      ;  P  = {!!}
+      ;  _==_ = λ {b} f g →   A [ char t < id1 A b , id1 A b > δmono  o < f , g > ]
+      ;  _∈_ = λ {a} x α →  A [ CCC.ε c o < α , x > ]
+      ;  _|-_  = {!!}
+      -- ;  isTL = {!!}
+    }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ToposSub.agda	Wed Apr 07 15:17:38 2021 +0900
@@ -0,0 +1,95 @@
+open import CCC
+open import Level
+open import Category
+open import cat-utility
+open import HomReasoning
+module ToposSub   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ c)) where
+
+  open Topos
+  open Equalizer
+  open ≈-Reasoning A
+  open CCC.CCC c
+
+  open Functor
+  open import Category.Sets hiding (_o_)
+  open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
+
+--             ○ b
+--       b -----------→ 1
+--       |              |
+--     m |              | ⊤
+--       ↓    char m    ↓
+--       a -----------→ Ω
+
+  record SubObject (a : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+     field
+        sb : Obj A
+        sm : Hom A sb a 
+        smono : Mono A sm
+
+  postulate
+    I : Set c₁
+    small : Small A I 
+
+  open import yoneda A I small
+
+
+  module SubObjectFunctor
+     (S : (a : Set (c₁ ⊔ c₂ ⊔ ℓ))  → Set c₂)
+     (solv← : {x : Obj A} → S (SubObject x) → SubObject x)
+     (solv→ : {x : Obj A} → SubObject x → S (SubObject x))
+     (soiso← : {a : Obj A} → (x : SubObject a) → solv← (solv→ x) ≡ x)
+     (soiso→ : {a : Obj A} → (x : S (SubObject a) ) → solv→ (solv← x) ≡ x)
+     (≡←≈ :   {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y) where
+
+    open SubObject 
+
+    Smap : {x y : Obj A} → Hom A y x → Hom Sets (S (SubObject x)) (S (SubObject y))
+    Smap {x} {y} h s = solv→ record { sb = y ; sm = id1 A y ; smono = record { isMono = λ f g eq → sm1 f g eq } } where
+         sm1 : {a : Obj A } → ( f g : Hom A a y ) → A [ A [ id1 A y o f ]  ≈ A [ id1 A y o g ] ] → A [ f  ≈ g ]
+         sm1 f g eq = begin
+              f ≈↑⟨ idL ⟩ 
+              id1 A y o f ≈⟨ eq ⟩ 
+              id1 A y o g ≈⟨ idL  ⟩ 
+              g ∎  
+
+    SubObjectFuntor  : Functor  (Category.op A)  (Sets {c₂})
+    SubObjectFuntor  = record {
+         FObj = λ x → S (SubObject x)
+       ; FMap = Smap
+       ; isFunctor  = record {
+              identity = {!!}
+            ; distr  = {!!}
+            ; ≈-cong  = {!!}
+          }
+       } 
+
+    open NTrans 
+    sub→topos : (Ω : Obj A) → Representable A ≡←≈ SubObjectFuntor Ω → Topos A c
+    sub→topos Ω R = record {
+          Ω =  Ω
+       ;  ⊤ = TMap (Representable.repr→ R) １ (solv→ record { sb = {!!} ; sm = {!!} ; smono = {!!} })
+       ;  Ker = λ {a} h → record { equalizer-c = sb {!!}
+          ; equalizer = sm {!!}
+          ; isEqualizer = {!!}
+          }
+       ;  char = λ m mono → {!!} 
+       ;  isTopos = record {
+          char-uniqueness  = {!!}
+       ;  ker-m = {!!}
+          } }
+ 
+    topos→rep : (t : Topos A c ) → Representable A ≡←≈ SubObjectFuntor (Topos.Ω t)
+    topos→rep t = record {
+        repr→ = record { TMap = λ a Sa → Topos.char t (sm (solv← Sa)) (smono (solv← Sa)) ; isNTrans = record { commute = {!!} } } -- Hom A a Ω
+      ; repr← = record { TMap = λ a h →  solv→ record {sb = equalizer-c (Ker t h) ; sm = equalizer (Ker t h) ; smono =
+         {!!} } ; isNTrans = {!!} }  -- FObj (Sub S) a
+      ; reprId→  = {!!}
+      ; reprId←  = {!!}
+     }
+ 
+ 
+
+
+
+