Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate filter.agda @ 276:6f10c47e4e7a
separate choice
fix sup-o
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 May 2020 09:02:52 +0900 |
| parents | 985a1af11bce |
| children | d9d3654baee1 |
| rev | line source |
|---|---|
| 190 | 1 open import Level |
| 236 | 2 open import Ordinals |
| 3 module filter {n : Level } (O : Ordinals {n}) where | |
| 4 | |
| 190 | 5 open import zf |
| 236 | 6 open import logic |
| 7 import OD | |
| 193 | 8 |
| 190 | 9 open import Relation.Nullary |
| 10 open import Relation.Binary | |
| 11 open import Data.Empty | |
| 12 open import Relation.Binary | |
| 13 open import Relation.Binary.Core | |
| 14 open import Relation.Binary.PropositionalEquality | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) |
|
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
16 |
| 236 | 17 open inOrdinal O |
| 18 open OD O | |
| 19 open OD.OD | |
| 190 | 20 |
| 236 | 21 open _∧_ |
| 22 open _∨_ | |
| 23 open Bool | |
| 24 | |
| 267 | 25 _∩_ : ( A B : OD ) → OD |
| 26 A ∩ B = record { def = λ x → def A x ∧ def B x } | |
| 27 | |
| 28 _∪_ : ( A B : OD ) → OD | |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
29 A ∪ B = record { def = λ x → def A x ∨ def B x } |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
30 |
| 270 | 31 _＼_ : ( A B : OD ) → OD |
| 32 A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) } | |
| 33 | |
| 34 | |
| 265 | 35 record Filter ( L : OD ) : Set (suc n) where |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
36 field |
| 270 | 37 filter : OD |
| 38 proper : ¬ ( filter ∋ od∅ ) | |
| 271 | 39 inL : filter ⊆ L |
| 40 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q | |
| 270 | 41 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
42 |
| 265 | 43 open Filter |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
44 |
| 270 | 45 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L |
| 46 L-filter {L} P {p} lt = filter1 P {p} {L} {!!} lt {!!} | |
| 190 | 47 |
| 270 | 48 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n |
| 49 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) | |
| 190 | 50 |
| 270 | 51 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n |
| 52 ultra-filter {L} P {p} = L ∋ p → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) | |
| 190 | 53 |
| 265 | 54 |
| 270 | 55 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q} |
| 56 filter-lemma1 {L} P {p} {q} u lt = {!!} | |
| 57 | |
| 58 filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter {L} P {p} | |
| 59 filter-lemma2 {L} P prime p with prime {!!} | |
| 60 ... | t = {!!} | |
| 266 | 61 |
| 267 | 62 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) |
| 266 | 63 generated-filter {L} P p = record { |
| 271 | 64 proper = {!!} ; |
| 270 | 65 filter = {!!} ; inL = {!!} ; |
| 66 filter1 = {!!} ; filter2 = {!!} | |
| 266 | 67 } |
| 68 | |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
69 record Dense (P : OD ) : Set (suc n) where |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
70 field |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
71 dense : OD |
| 271 | 72 incl : dense ⊆ P |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
73 dense-f : OD → OD |
| 271 | 74 dense-p : { p : OD} → P ∋ p → p ⊆ (dense-f p) |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
75 |
| 266 | 76 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) |
| 77 | |
| 78 infinite = ZF.infinite OD→ZF | |
| 79 | |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
80 module in-countable-ordinal {n : Level} where |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
81 |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
82 import ordinal |
| 266 | 83 |
| 276 | 84 -- open ordinal.C-Ordinal-with-choice |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
85 |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
86 Hω2 : Filter (Power (Power infinite)) |
| 270 | 87 Hω2 = {!!} |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
88 |