Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate filter.agda @ 267:e469de3ae7cc
⊆
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 30 Sep 2019 20:59:45 +0900 |
| parents | 0d7d6e4da36f |
| children | 7b4a66710cdd |
| 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 | |
| 29 A ∪ B = Union (A , B) | |
| 30 | |
| 265 | 31 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
|
32 field |
| 267 | 33 F1 : { p q : OD } → L ∋ p → ({ x : OD} → _⊆_ p q {x} ) → L ∋ q |
| 34 F2 : { p q : OD } → L ∋ p → L ∋ q → L ∋ (p ∩ q) | |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
35 |
| 265 | 36 open Filter |
|
191
9eb6a8691f02
choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
190
diff
changeset
|
37 |
| 265 | 38 proper-filter : {L : OD} → Filter L → Set n |
| 267 | 39 proper-filter {L} P = ¬ ( L ∋ od∅ ) |
| 190 | 40 |
| 267 | 41 prime-filter : {L : OD} → Filter L → {p q : OD } → Set n |
| 42 prime-filter {L} P {p} {q} = L ∋ ( p ∪ q) → ( L ∋ p ) ∨ ( L ∋ q ) | |
| 190 | 43 |
| 267 | 44 ultra-filter : {L : OD} → Filter L → {p : OD } → Set n |
| 45 ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p )) | |
| 190 | 46 |
| 265 | 47 postulate |
| 267 | 48 dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡ ( p ∩ q ) ∪ ( p ∩ r ) |
| 265 | 49 |
| 267 | 50 filter-lemma1 : {L : OD} → (P : Filter L) → {p q : OD } → ( (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q} |
| 266 | 51 filter-lemma1 {L} P {p} {q} u lt with u p | u q |
| 52 filter-lemma1 {L} P {p} {q} u lt | case1 x | case1 y = case1 x | |
| 53 filter-lemma1 {L} P {p} {q} u lt | case1 x | case2 y = case1 x | |
| 54 filter-lemma1 {L} P {p} {q} u lt | case2 x | case1 y = case2 y | |
| 267 | 55 filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y = ⊥-elim ( y ? ) |
| 266 | 56 |
| 267 | 57 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } ) |
| 266 | 58 generated-filter {L} P p = record { |
| 59 F1 = {!!} ; F2 = {!!} | |
| 60 } | |
| 61 | |
| 62 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) | |
| 63 | |
| 64 infinite = ZF.infinite OD→ZF | |
| 65 | |
| 66 Hω2 : Filter (Power (Power infinite)) | |
| 67 Hω2 = {!!} | |
| 68 |