Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 300:e70980bd80c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
-- the set of finite partial functions from ω to 2
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Jun 2020 15:12:43 +0900
parents 42f89e5efb00
children b012a915bbb5
files OD.agda filter.agda
diffstat 2 files changed, 17 insertions(+), 28 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Jun 15 18:15:48 2020 +0900
+++ b/OD.agda	Tue Jun 23 15:12:43 2020 +0900
@@ -208,8 +208,8 @@
 ZFSubset : (A x : OD  ) → OD 
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  --   roughly x = A → Set 
 
-Def :  (A :  OD ) → OD 
-Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A x) ) )   
+OPwr :  (A :  OD ) → OD 
+OPwr  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A x) ) )   
 
 -- _⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
 -- _⊆_ A B {x} = A ∋ x →  B ∋ x
@@ -268,7 +268,7 @@
     _∈_ : ( A B : ZFSet  ) → Set n
     A ∈ B = B ∋ A
     Power : OD  → OD 
-    Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
+    Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
     -- ｛_｝ : ZFSet → ZFSet
     -- ｛ x ｝ = ( x ,  x )     -- it works but we don't use 
 
@@ -369,11 +369,11 @@
          -- 
          -- Transitive Set case
          -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t == t
-         -- Def (Ord a) is a sup of ZFSubset (Ord a) t, so Def (Ord a) ∋ t
-         -- Def  A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
+         -- OPwr (Ord a) is a sup of ZFSubset (Ord a) t, so OPwr (Ord a) ∋ t
+         -- OPwr  A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
          -- 
-         ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
-         ord-power← a t t→A  = def-subst  {_} {_} {Def (Ord a)} {od→ord t}
+         ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
+         ord-power← a t t→A  = def-subst  {_} {_} {OPwr (Ord a)} {od→ord t}
                  lemma refl (lemma1 lemma-eq )where
               lemma-eq :  ZFSubset (Ord a) t == t
               eq→ lemma-eq {z} w = proj2 w 
@@ -387,10 +387,10 @@
               lemma = sup-o<  
 
          -- 
-         -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first
+         -- Every set in OD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
          -- then replace of all elements of the Power set by A ∩ y
          -- 
-         -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y )
+         -- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y )
 
          -- we have oly double negation form because of the replacement axiom
          --
@@ -398,7 +398,7 @@
          power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
               a = od→ord A
               lemma2 : ¬ ( (y : OD) → ¬ (t ==  (A ∩ y)))
-              lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t
+              lemma2 = replacement→ (OPwr (Ord (od→ord A))) t P∋t
               lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x)
               lemma3 y eq not = not (proj1 (eq→ eq t∋x))
               lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y)))
@@ -411,7 +411,7 @@
               a = od→ord A
               lemma0 : {x : OD} → t ∋ x → Ord a ∋ x
               lemma0 {x} t∋x = c<→o< (t→A t∋x)
-              lemma3 : Def (Ord a) ∋ t
+              lemma3 : OPwr (Ord a) ∋ t
               lemma3 = ord-power← a t lemma0
               lemma4 :  (A ∩ ord→od (od→ord t)) ≡ t
               lemma4 = let open ≡-Reasoning in begin
@@ -424,7 +424,7 @@
               lemma1 : od→ord t o< sup-o  (λ x → od→ord (A ∩ x))
               lemma1 = subst (λ k → od→ord k o< sup-o   (λ x → od→ord (A ∩ x)))
                   lemma4 (sup-o<  {λ x → od→ord (A ∩ x)}  )
-              lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
+              lemma2 :  def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
               lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
                   lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
                   lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
--- a/filter.agda	Mon Jun 15 18:15:48 2020 +0900
+++ b/filter.agda	Tue Jun 23 15:12:43 2020 +0900
@@ -119,28 +119,17 @@
         lemma : (p : OD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
         lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
 
-generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
-generated-filter {L} P p = {!!}
-
 record Dense  (P : OD ) : Set (suc n) where
    field
        dense : OD
        incl :  dense ⊆ P 
        dense-f : OD → OD
-       dense-p :  { p : OD} → P ∋ p  → p ⊆ (dense-f p) 
-
--- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
-
-infinite = ZF.infinite OD→ZF
+       dense-d :  { p : OD} → P ∋ p  → dense ∋ dense-f p  
+       dense-p :  { p : OD} → P ∋ p  →  p ⊆ (dense-f p) 
 
-module in-countable-ordinal {n : Level} where
-
-   import ordinal
-
-   -- open  ordinal.C-Ordinal-with-choice 
-
-   Hω2 : Filter (Power (Power infinite))
-   Hω2 = {!!}
+--    the set of finite partial functions from ω to 2
+--
+-- Hω2 : Filter (Power (Power infinite))
 
 
 record Ideal  ( L : OD  ) : Set (suc n) where