Mercurial > hg > Members > kono > Proof > category

changeset 1045:139d58917093

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 Fri, 09 Apr 2021 10:26:01 +0900
parents aa3ec90f5b78
children 60b24b3dc0c6
files src/ToposIL.agda
diffstat 1 files changed, 3 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposIL.agda	Fri Apr 09 09:51:02 2021 +0900
+++ b/src/ToposIL.agda	Fri Apr 09 10:26:01 2021 +0900
@@ -53,12 +53,14 @@
 
   open import ToposEx A c using ( δmono  )
 
-  -- λ (x ∈ a) → φ x
+  -- f ≡ λ (x ∈ a) → φ x or  ∃ (f : b <= a) →  f ∙ x ≈  φ x  
   record Select  {a b : Obj A} (Ω : Obj A) (α : Hom A (CCC.１ c) (Ω <= 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) (b <= a) 
       isSelect : (x : Hom A  (CCC.１ c) a  ) → A [  A [ CCC.ε c o < sl , x > ]  ≈  φ x ]
+      -- isUnique : (x : Hom A  (CCC.１ c) a  ) → (f : Hom A (CCC.１ c) (b <= a) )  → A [  A [ CCC.ε c o < f , x > ]  ≈  φ x ]
+      --   →  A [ sl  ≈ f ]
 
   -- functional completeness
   FC : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )