Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate filter.agda @ 293:9972bd4a0d6f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 14 Jun 2020 08:57:14 +0900 |
| parents | 773e03dfd6ed |
| children | 4340ffcfa83d |
| 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⊔_ ) |
| 293 | 16 import BAlgbra |
| 17 | |
| 18 open BAlgbra O | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
19 |
| 236 | 20 open inOrdinal O |
| 21 open OD O | |
| 22 open OD.OD | |
|
277
d9d3654baee1
seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
276
diff
changeset
|
23 open ODAxiom odAxiom |
| 190 | 24 |
| 236 | 25 open _∧_ |
| 26 open _∨_ | |
| 27 open Bool | |
| 28 | |
| 292 | 29 -- Kunen p.76 and p.53 |
| 265 | 30 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
|
31 field |
| 290 | 32 filter : OD |
| 33 f⊆PL : filter ⊆ Power L | |
| 271 | 34 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q |
| 270 | 35 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
|
36 |
| 292 | 37 open Filter |
| 38 | |
| 293 | 39 -- should use inhabit? |
| 292 | 40 proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n |
| 293 | 41 proper-filter {L} P {p} = ¬ (filter P ∋ od∅) |
| 292 | 42 |
| 43 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n | |
| 44 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) | |
| 45 | |
| 293 | 46 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set (suc n ) |
| 47 ultra-filter {L} P {p} = p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L ＼ p) ) | |
| 265 | 48 |
| 270 | 49 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q} |
| 293 | 50 filter-lemma1 {L} P {p} {q} u lt with lt |
| 270 | 51 ... | t = {!!} |
| 266 | 52 |
| 293 | 53 filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter {L} P {p} |
| 54 filter-lemma2 {L} P prime p = {!!} | |
| 55 | |
| 267 | 56 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) |
| 293 | 57 generated-filter {L} P p = {!!} |
| 266 | 58 |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
59 record Dense (P : OD ) : Set (suc n) where |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
60 field |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
61 dense : OD |
| 271 | 62 incl : dense ⊆ P |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
63 dense-f : OD → OD |
| 271 | 64 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
|
65 |
| 266 | 66 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) |
| 67 | |
| 68 infinite = ZF.infinite OD→ZF | |
| 69 | |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
70 module in-countable-ordinal {n : Level} where |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
71 |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
72 import ordinal |
| 266 | 73 |
| 276 | 74 -- open ordinal.C-Ordinal-with-choice |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
75 |
|
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
76 Hω2 : Filter (Power (Power infinite)) |
| 270 | 77 Hω2 = {!!} |
|
269
30e419a2be24
disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
268
diff
changeset
|
78 |
| 293 | 79 |
| 80 record Ideal ( L : OD ) : Set (suc n) where | |
| 81 field | |
| 82 ideal : OD | |
| 83 i⊆PL : ideal ⊆ Power L | |
| 84 ideal1 : { p q : OD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q | |
| 85 ideal2 : { p q : OD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) | |
| 86 | |
| 87 open Ideal | |
| 88 | |
| 89 proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n | |
| 90 proper-ideal {L} P {p} = ideal P ∋ od∅ | |
| 91 | |
| 92 prime-ideal : {L : OD} → Ideal L → ∀ {p q : OD } → Set n | |
| 93 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) | |
| 94 |