### changeset 300:e70980bd80c7

-- the set of finite partial functions from ω to 2
author Shinji KONO Tue, 23 Jun 2020 15:12:43 +0900 42f89e5efb00 b012a915bbb5 OD.agda filter.agda 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```