annotate filter.agda @ 370:1425104bb5d8

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 19 Jul 2020 12:26:17 +0900
parents 30de2d9b93c1
children e75402b1f7d4
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
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
9 open import Relation.Nullary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
10 open import Relation.Binary
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
11 open import Data.Empty
190
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
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
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⊔_ )
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
16 import BAlgbra
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
17
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
20 open inOrdinal O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
21 open OD O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
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
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
25 import ODC
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
26
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
27 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
28 open _∨_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
29 open Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
30
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
31 -- Kunen p.76 and p.53, we use ⊆
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
32 record Filter ( L : HOD ) : 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
33 field
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
34 filter : HOD
290
359402cc6c3d definition of filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
35 f⊆PL : filter ⊆ Power L
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
36 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
37 filter2 : { p q : HOD } → 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
38
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
39 open Filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
40
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
41 record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
42 field
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
43 proper : ¬ (filter P ∋ od∅)
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
44 prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
45
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
46 record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
47 field
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
48 proper : ¬ (filter P ∋ od∅)
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
49 ultra : {p : HOD } → p ⊆ L → ( filter P ∋ p ) ∨ ( filter P ∋ ( L \ p) )
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
50
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
51 open _⊆_
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
52
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
53 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
54 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
55
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
56 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
57 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
58 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x)
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
59 t1 = zf.IsZF.power→ isZF A t PA∋t
292
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
60
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
61 ∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
62 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
63
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
64 ∪-lemma1 : {L p q : HOD } → (p ∪ q) ⊆ L → p ⊆ L
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
65 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
66
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
67 ∪-lemma2 : {L p q : HOD } → (p ∪ q) ⊆ L → q ⊆ L
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
68 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
69
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
70 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
71 q∩q⊆q = record { incl = λ lt → proj1 lt }
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
72
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
73 open HOD
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
74
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
75 -----
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
76 --
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
77 -- ultra filter is prime
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
78 --
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
79
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
80 filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
81 filter-lemma1 {L} P u = record {
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
82 proper = ultra-filter.proper u
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
83 ; prime = lemma3
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
84 } where
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
85 lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
86 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
87 ... | case1 p∈P = case1 p∈P
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
88 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
89 lemma5 : ((p ∪ q ) ∩ (L \ p)) =h= (q ∩ (L \ p))
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
90 lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
91 ; eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
92 } where
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
93 lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L \ p)) x → odef q x
294
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
94 lemma4 x lt with proj1 lt
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
95 lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
96 lemma4 x lt | case2 qx = qx
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
97 lemma6 : filter P ∋ ((p ∪ q ) ∩ (L \ p))
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
98 lemma6 = filter2 P lt ¬p∈P
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
99 lemma7 : filter P ∋ (q ∩ (L \ p))
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
100 lemma7 = subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
101 lemma8 : (q ∩ (L \ p)) ⊆ q
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
102 lemma8 = q∩q⊆q
4340ffcfa83d ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 293
diff changeset
103
295
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
104 -----
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
105 --
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
106 -- if Filter contains L, prime filter is ultra
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
107 --
822b50091a26 fix prime
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
108
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
109 filter-lemma2 : {L : HOD} → (P : Filter L) → filter P ∋ L → prime-filter P → ultra-filter P
296
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
110 filter-lemma2 {L} P f∋L prime = record {
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
111 proper = prime-filter.proper prime
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
112 ; ultra = λ {p} p⊆L → prime-filter.prime prime (lemma p p⊆L)
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
113 } where
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
114 open _==_
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
115 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L \ p))
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
116 eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
296
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
117 eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
118 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
331
12071f79f3cf HOD done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
119 eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x ))
296
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
120 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
121 lemma : (p : HOD) → p ⊆ L → filter P ∋ (p ∪ (L \ p))
296
42f89e5efb00 if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
122 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
123
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
124 record Dense (P : HOD ) : Set (suc n) where
269
30e419a2be24 disjunction and conjunction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 268
diff changeset
125 field
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
126 dense : HOD
368
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
127 incl : dense ⊆ Power P
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
128 dense-f : HOD → HOD
368
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
129 dense-d : { p : HOD} → p ⊆ P → dense ∋ dense-f p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
130 dense-p : { p : HOD} → p ⊆ P → p ⊆ (dense-f p)
266
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 265
diff changeset
131
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
132 record Ideal ( L : HOD ) : Set (suc n) where
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
133 field
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
134 ideal : HOD
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
135 i⊆PL : ideal ⊆ Power L
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
136 ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
137 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q)
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
139 open Ideal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
140
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
141 proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
142 proper-ideal {L} P {p} = ideal P ∋ od∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
143
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
144 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
293
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
145 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 292
diff changeset
146
364
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 363
diff changeset
147 -------
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
148 -- the set of finite partial functions from ω to 2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
149 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
150 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
151
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
152 import OPair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
153 open OPair O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
154
370
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
155 data Two : Set n where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
156 i0 : Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
157 i1 : Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
158
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
159 record PFunc : Set (suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
160 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
161 restrict : Nat → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
162 map : (x : Nat ) → restrict x → Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
163
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
164 open PFunc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
165
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
166 record _f⊆_ (f g : PFunc) : Set (suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
167 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
168 feq : (x : Nat) → (fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
169
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
170 full-func : Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
171 full-func = Nat → Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
173 full→PF : (Nat → Two) → PFunc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
174 full→PF f = record { restrict = λ x → One ; map = λ x _ → f x }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
175
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
176 _↑_ : (Nat → Two) → Nat → PFunc
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
177 f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
178
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
179 record F-Filter (PL : Set n) (L : PL ) ( _⊆_ : PL → PL → Set n) ( _∋_ : PL → PL → Set n) : Set (suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
180 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
181 filter : PL
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
182 f⊆PL : filter ⊆ L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
183 filter1 : { p q : PL } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
184 filter2 : { p q : PL } → filter ∋ p → filter ∋ q → (filter ∋ p) ∧ (filter ∋ q)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
185
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
186 ODSuc : (y : HOD) → infinite ∋ y → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
187 ODSuc y lt = Union (y , (y , y))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
188
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
189 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
190 hφ : Hω2 0 o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
191 h0 : {i : Nat} {x : Ordinal } → Hω2 i x →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
192 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
193 h1 : {i : Nat} {x : Ordinal } → Hω2 i x →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
194 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x )))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
195 he : {i : Nat} {x : Ordinal } → Hω2 i x →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
196 Hω2 (Suc i) x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
197
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
198 record Hω2r (x : Ordinal) : Set n where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
199 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
200 count : Nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
201 hω2 : Hω2 count x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
202
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
203 open Hω2r
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
204
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
205 HODω2 : HOD
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
206 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
207 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
208 ω<next = ω<next-o∅ ho<
366
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
209 lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
210 lemma = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
211 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
212 odmax0 {y} r with hω2 r
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
213 ... | hφ = x<nx
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
214 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
215 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
216 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
217
370
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
218 ω→2 : HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
219 ω→2 = Replace (Power infinite) (λ p p⊆i → Replace infinite (λ x i∋x → < x , repl p x > )) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
220 repl : HOD → HOD → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
221 repl p x with ODC.∋-p O p x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
222 ... | yes _ = nat→ω 1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
223 ... | no _ = nat→ω 0
368
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
224
370
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
225 record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
226 -- field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
227 -- n : HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
228 -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
229
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
230 Gf : {f : HOD} → ω→2 ∋ f → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 368
diff changeset
231 Gf {f} lt = Select HODω2 (λ x H∋x → {!!} )
368
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
232
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
233 G : (Nat → Two) → Filter HODω2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
234 G f = record {
365
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
235 filter = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
236 ; f⊆PL = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
237 ; filter1 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
238 ; filter2 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
239 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
240 filter0 : HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
241 filter0 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
242 f⊆PL1 : filter0 ⊆ Power HODω2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
243 f⊆PL1 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
244 filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
245 filter11 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
246 filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
247 filter12 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 364
diff changeset
248
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
249 -- the set of finite partial functions from ω to 2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
250
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
251 Hω2f : Set (suc n)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
252 Hω2f = (Nat → Set n) → Two
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
253
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
254 Hω2f→Hω2 : Hω2f → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
255 Hω2f→Hω2 p = record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
256
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 331
diff changeset
257