Mercurial > hg > Members > kono > Proof > category

changeset 1040:d252240ccd1e

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 Thu, 08 Apr 2021 16:19:00 +0900
parents 572de732853f
children c3e6fddb04e8
files src/ToposIL.agda
diffstat 1 files changed, 3 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposIL.agda	Wed Apr 07 16:00:24 2021 +0900
+++ b/src/ToposIL.agda	Thu Apr 08 16:19:00 2021 +0900
@@ -54,7 +54,7 @@
   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 ) → {!!} )
+  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)
@@ -64,9 +64,10 @@
   topos→logic = record {
          Ω = Topos.Ω t
       ;  ⊤ = Topos.⊤ t
-      ;  P  = {!!}
+      ;  P  = λ a → (Topos.Ω t) <= a
       ;  _==_ = λ {b} f g →   A [ char t < id1 A b , id1 A b > δmono  o < f , g > ]
       ;  _∈_ = λ {a} x α →  A [ CCC.ε c o < α , x > ]
+      -- { x ∈ a | φ x } : P a
       ;  select = λ {a} α φ →  Select.sl {!!}
       ;  _|-_  = λ {a} x → {!!}
       -- ;  isTL = {!!}