Mercurial > hg > Members > kono > Proof > category

changeset 1041:c3e6fddb04e8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
internal language written
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 09 Apr 2021 09:05:59 +0900
parents d252240ccd1e
children a929a58a389d
files src/ToposIL.agda
diffstat 1 files changed, 14 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposIL.agda	Thu Apr 08 16:19:00 2021 +0900
+++ b/src/ToposIL.agda	Fri Apr 09 09:05:59 2021 +0900
@@ -26,7 +26,7 @@
   --    field
   --        a : {!!}
 
-  record Logic    (c : CCC A)  :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+  record Logic :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
          Ω : Obj A
          ⊤ : Hom A (CCC.１ c) Ω
@@ -34,9 +34,10 @@
          _==_ : {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 {!!} Ω
+         select : {a b : Obj A}  (α : Hom A (CCC.１ c) (P a) ) → ( (x :  Hom A  (CCC.１ c) a ) →  Hom A (CCC.１ c) Ω ) → Hom A (CCC.１ c) (P a)
          -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
+     _|-_  : {a : Obj A} (p : Hom A (CCC.１ c) (Ω t )) → Set ℓ
+     _|-_  {a} p = A [ p ≈  Topos.⊤ t ] 
   
 --             ○ b
 --       b -----------→ 1
@@ -54,21 +55,24 @@
   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  {a b : Obj A}  (α : Hom A (CCC.１ c) ((Topos.Ω t) <= a) ) ( φ : (x :  Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) b )
          :  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 ]
+      sl :  Hom A (CCC.１ c) (b <= a) 
+      isSelect : (x : Hom A  (CCC.１ c) a  ) → A [  A [ CCC.ε c o < sl , x > ]  ≈  φ x ]
 
-  topos→logic : Logic c
-  topos→logic = record {
+  -- functional completeness
+  FC : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
+  FC = {a b : Obj A}  (α : Hom A (CCC.１ c) ((Topos.Ω t) <= a) ) ( φ : (x :  Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) b ) → Select α φ
+
+  topos→logic : FC  → Logic 
+  topos→logic fc = record {
          Ω = Topos.Ω t
       ;  ⊤ = Topos.⊤ t
       ;  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 → {!!}
+      ;  select = λ {a} α φ →  Select.sl ( fc α φ )
       -- ;  isTL = {!!}
     }