# HG changeset patch # User Shinji KONO # Date 1592892763 -32400 # Node ID e70980bd80c76c7a021641dfa3628e502644738e # Parent 42f89e5efb00569c5edce3ea795853e91386dc32 -- the set of finite partial functions from ω to 2 diff -r 42f89e5efb00 -r e70980bd80c7 OD.agda --- 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 ))) diff -r 42f89e5efb00 -r e70980bd80c7 filter.agda --- 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