annotate filter.agda @ 291:ef93c56ad311

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 12 Jun 2020 19:21:14 +0900
parents 359402cc6c3d 5de8905a5a2b
children 773e03dfd6ed
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
2 open import Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
3 module filter {n : Level } (O : Ordinals {n}) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
4
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import zf
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
6 open import logic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
7 import OD
193
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
8
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Nullary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Empty
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Relation.Binary.Core
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
17 open inOrdinal O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
18 open OD O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
19 open OD.OD
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 276
diff changeset
20 open ODAxiom odAxiom
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
22 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
23 open _∨_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
24 open Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
25
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
26 _∩_ : ( A B : OD ) → OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
27 A ∩ B = record { def = λ x → def A x ∧ def B x }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
28
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
29 _∪_ : ( A B : OD ) → OD
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
30 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
31
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
32 _\_ : ( A B : OD ) → OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
33 A \ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
34
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
35
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
36 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
37 field
290
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
38 filter : OD
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
39 ¬f∋∅ : ¬ ( filter ∋ od∅ )
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
40 f∋L : filter ∋ L
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
41 f⊆PL : filter ⊆ Power L
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
42 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
43 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
44
290
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
45 record Ideal ( L : OD ) : Set (suc n) where
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
46 field
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
47 ideal : OD
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
48 i∋∅ : ideal ∋ od∅
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
49 ¬i∋L : ¬ ( ideal ∋ L )
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
50 i⊆PL : ideal ⊆ Power L
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
51 ideal1 : { p q : OD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
52 ideal2 : { p q : OD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q)
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
53
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
54 open Filter
290
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
55 open Ideal
287
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
56
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
57 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
290
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
58 L-filter {L} P {p} lt = {!!} -- filter1 P {p} {L} {!!} lt {!!}
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
60 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
61 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
63 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
64 ultra-filter {L} P {p} = L ∋ p → ( filter P ∋ p ) ∨ ( filter P ∋ ( L \ p) )
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
66
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
67 filter-lemma1 : {L : OD} → (P : Filter L) → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
68 filter-lemma1 {L} P {p} {q} u lt = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
69
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
70 filter-lemma2 : {L : OD} → (P : Filter L) → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) → ∀ (p : OD ) → ultra-filter {L} P {p}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
71 filter-lemma2 {L} P prime p with prime {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
72 ... | t = {!!}
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
73
267
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 266
diff changeset
74 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
75 generated-filter {L} P p = record {
290
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
76 filter = {!!} ;
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
77 filter1 = {!!} ; filter2 = {!!}
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
78 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
79
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
80 record Dense (P : OD ) : Set (suc n) where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
81 field
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
82 dense : OD
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
83 incl : dense ⊆ P
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
84 dense-f : OD → OD
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 270
diff changeset
85 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
86
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
87 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
88
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
89 infinite = ZF.infinite OD→ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
90
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
91 module in-countable-ordinal {n : Level} where
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
92
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
93 import ordinal
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
94
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 272
diff changeset
95 -- open ordinal.C-Ordinal-with-choice
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
96
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
97 Hω2 : Filter (Power (Power infinite))
270
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 269
diff changeset
98 Hω2 = {!!}
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
99