Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison filter.agda @ 365:7f919d6b045b
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 18 Jul 2020 12:29:38 +0900 |
parents | 67580311cc8e |
children | 1a8ca713bc32 |
comparison
equal
deleted
inserted
replaced
364:67580311cc8e | 365:7f919d6b045b |
---|---|
69 | 69 |
70 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q | 70 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q |
71 q∩q⊆q = record { incl = λ lt → proj1 lt } | 71 q∩q⊆q = record { incl = λ lt → proj1 lt } |
72 | 72 |
73 open HOD | 73 open HOD |
74 _=h=_ : (x y : HOD) → Set n | |
75 x =h= y = od x == od y | |
76 | 74 |
77 ----- | 75 ----- |
78 -- | 76 -- |
79 -- ultra filter is prime | 77 -- ultra filter is prime |
80 -- | 78 -- |
155 open OPair O | 153 open OPair O |
156 | 154 |
157 ODSuc : (y : HOD) → infinite ∋ y → HOD | 155 ODSuc : (y : HOD) → infinite ∋ y → HOD |
158 ODSuc y lt = Union (y , (y , y)) | 156 ODSuc y lt = Union (y , (y , y)) |
159 | 157 |
160 nat→ω : Nat → HOD | 158 postulate |
161 nat→ω Zero = od∅ | |
162 nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) | |
163 | |
164 postulate -- we have proved in other module | |
165 ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n)) | |
166 ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅ | |
167 | |
168 postulate | |
169 ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) | 159 ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) |
160 | |
170 | 161 |
171 data Hω2 : ( x : Ordinal ) → Set n where | 162 data Hω2 : ( x : Ordinal ) → Set n where |
172 hφ : Hω2 o∅ | 163 hφ : Hω2 o∅ |
173 h0 : {x : Ordinal } → Hω2 x → | 164 h0 : {x : Ordinal } → Hω2 x → |
174 Hω2 (od→ord < nat→ω 0 , ord→od x >) | 165 Hω2 (od→ord < nat→ω 0 , ord→od x >) |
177 h2 : {x : Ordinal } → Hω2 x → | 168 h2 : {x : Ordinal } → Hω2 x → |
178 Hω2 (od→ord < nat→ω 2 , ord→od x >) | 169 Hω2 (od→ord < nat→ω 2 , ord→od x >) |
179 | 170 |
180 HODω2 : HOD | 171 HODω2 : HOD |
181 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where | 172 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where |
173 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅ | |
174 ω<next = ω<next-o∅ ho< | |
182 lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n → od→ord < ord→od n , ord→od y > o< next y | 175 lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n → od→ord < ord→od n , ord→od y > o< next y |
183 lemma0 {n} {y} hw2 inf = nexto=n {!!} | 176 lemma0 {n} {y} hw2 inf = nexto=n {!!} |
184 odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅ | 177 odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅ |
185 odmax0 {o∅} hφ = x<nx | 178 odmax0 {o∅} hφ = x<nx |
186 odmax0 (h0 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {0} ))) | 179 odmax0 (h0 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {0} ))) |
187 odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {1} ))) | 180 odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {1} ))) |
188 odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {2} ))) | 181 odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k → od→ord < k , ord→od y >) oiso ) (lemma0 lt (ω∋nat→ω {2} ))) |
189 | 182 |
183 HODω2-Filter : Filter HODω2 | |
184 HODω2-Filter = record { | |
185 filter = {!!} | |
186 ; f⊆PL = {!!} | |
187 ; filter1 = {!!} | |
188 ; filter2 = {!!} | |
189 } where | |
190 filter0 : HOD | |
191 filter0 = {!!} | |
192 f⊆PL1 : filter0 ⊆ Power HODω2 | |
193 f⊆PL1 = {!!} | |
194 filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q | |
195 filter11 = {!!} | |
196 filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q) | |
197 filter12 = {!!} | |
198 | |
190 -- the set of finite partial functions from ω to 2 | 199 -- the set of finite partial functions from ω to 2 |
191 | 200 |
192 data Two : Set n where | 201 data Two : Set n where |
193 i0 : Two | 202 i0 : Two |
194 i1 : Two | 203 i1 : Two |