Mercurial > hg > Members > kono > Proof > category

changeset 1039:572de732853f

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 16:00:24 +0900
parents db3e89065178
children d252240ccd1e
files src/ToposIL.agda
diffstat 1 files changed, 12 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposIL.agda	Wed Apr 07 15:17:38 2021 +0900
+++ b/src/ToposIL.agda	Wed Apr 07 16:00:24 2021 +0900
@@ -33,6 +33,8 @@
          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) Ω
+         -- { x ∈ a | φ x } : P a
+         select : {a : Obj A}  (α : Hom A (CCC.１ c) (P a) ) → ( (x :  Hom A  (CCC.１ c) a ) → Set c₁) → Hom A (CCC.１ c) (P a)
          _|-_  : {a : Obj A} (x : List ( Hom A (CCC.１ c) a ) ) → Hom A {!!} Ω
          -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
   
@@ -51,6 +53,13 @@
 
   open import ToposEx A c t n using ( δmono  )
 
+  -- λ (x ∈ a) → φ x
+  record Select (P  : Obj A → Obj A ) {a : Obj A}  (α : Hom A (CCC.１ c) (P a) ) ( φ : (x :  Hom A  (CCC.１ c) a ) → {!!} )
+         :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+    field
+      sl :  Hom A (CCC.１ c) (P a)
+      isSelect : (x : Hom A  (CCC.１ c) a  ) → A [  A [ CCC.ε c o {!!} ]  ≈  φ x ]
+
   topos→logic : Logic c
   topos→logic = record {
          Ω = Topos.Ω t
@@ -58,6 +67,7 @@
       ;  P  = {!!}
       ;  _==_ = λ {b} f g →   A [ char t < id1 A b , id1 A b > δmono  o < f , g > ]
       ;  _∈_ = λ {a} x α →  A [ CCC.ε c o < α , x > ]
-      ;  _|-_  = {!!}
+      ;  select = λ {a} α φ →  Select.sl {!!}
+      ;  _|-_  = λ {a} x → {!!}
       -- ;  isTL = {!!}
-    }
+    }