Mercurial > hg > Members > kono > Proof > ZF-in-agda
annotate filter.agda @ 379:7b6592f0851a
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 21 Jul 2020 02:19:07 +0900 |
parents | 8cade5f660bd |
children | 0a116938a564 |
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 |
363 | 9 open import Relation.Nullary |
10 open import Relation.Binary | |
11 open import Data.Empty | |
190 | 12 open import Relation.Binary |
13 open import Relation.Binary.Core | |
363 | 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 | 16 import BAlgbra |
293 | 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 |
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 | 27 open _∧_ |
28 open _∨_ | |
29 open Bool | |
30 | |
295 | 31 -- Kunen p.76 and p.53, we use ⊆ |
329 | 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 | 34 filter : HOD |
290 | 35 f⊆PL : filter ⊆ Power L |
329 | 36 filter1 : { p q : HOD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q |
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 | 39 open Filter |
40 | |
329 | 41 record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where |
295 | 42 field |
43 proper : ¬ (filter P ∋ od∅) | |
329 | 44 prime : {p q : HOD } → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) |
292 | 45 |
329 | 46 record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where |
295 | 47 field |
48 proper : ¬ (filter P ∋ od∅) | |
329 | 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 | 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 |
374 | 56 refl-⊆ : {A : HOD} → A ⊆ A |
57 refl-⊆ {A} = record { incl = λ x → x } | |
58 | |
329 | 59 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A |
331 | 60 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where |
329 | 61 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
|
62 t1 = zf.IsZF.power→ isZF A t PA∋t |
292 | 63 |
329 | 64 ∈-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
|
65 ∈-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
|
66 |
329 | 67 ∪-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
|
68 ∪-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
|
69 |
329 | 70 ∪-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
|
71 ∪-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
|
72 |
329 | 73 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
|
74 q∩q⊆q = record { incl = λ lt → proj1 lt } |
265 | 75 |
331 | 76 open HOD |
77 | |
295 | 78 ----- |
79 -- | |
80 -- ultra filter is prime | |
81 -- | |
294
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
82 |
329 | 83 filter-lemma1 : {L : HOD} → (P : Filter L) → ∀ {p q : HOD } → ultra-filter P → prime-filter P |
295 | 84 filter-lemma1 {L} P u = record { |
85 proper = ultra-filter.proper u | |
86 ; prime = lemma3 | |
87 } where | |
329 | 88 lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) |
295 | 89 lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) ) |
90 ... | case1 p∈P = case1 p∈P | |
91 ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L \ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where | |
331 | 92 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
|
93 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
|
94 ; 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
|
95 } where |
331 | 96 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
|
97 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
|
98 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
|
99 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
|
100 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
|
101 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
|
102 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
|
103 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
|
104 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
|
105 lemma8 = q∩q⊆q |
4340ffcfa83d
ultra-filter P → prime-filter P done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
293
diff
changeset
|
106 |
295 | 107 ----- |
108 -- | |
109 -- if Filter contains L, prime filter is ultra | |
110 -- | |
111 | |
329 | 112 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
|
113 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
|
114 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
|
115 ; 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
|
116 } where |
42f89e5efb00
if Filter contains L, prime filter is ultra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
295
diff
changeset
|
117 open _==_ |
331 | 118 p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L \ p)) |
119 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
|
120 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
|
121 eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p }) |
331 | 122 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
|
123 eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p ) = proj1 ¬p |
329 | 124 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
|
125 lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L |
293 | 126 |
329 | 127 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
|
128 field |
329 | 129 dense : HOD |
379 | 130 d⊆P : dense ⊆ Power P |
329 | 131 dense-f : HOD → HOD |
368 | 132 dense-d : { p : HOD} → p ⊆ P → dense ∋ dense-f p |
133 dense-p : { p : HOD} → p ⊆ P → p ⊆ (dense-f p) | |
266 | 134 |
329 | 135 record Ideal ( L : HOD ) : Set (suc n) where |
293 | 136 field |
329 | 137 ideal : HOD |
293 | 138 i⊆PL : ideal ⊆ Power L |
329 | 139 ideal1 : { p q : HOD } → q ⊆ L → ideal ∋ p → q ⊆ p → ideal ∋ q |
140 ideal2 : { p q : HOD } → ideal ∋ p → ideal ∋ q → ideal ∋ (p ∪ q) | |
293 | 141 |
142 open Ideal | |
143 | |
329 | 144 proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n |
293 | 145 proper-ideal {L} P {p} = ideal P ∋ od∅ |
146 | |
329 | 147 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n |
293 | 148 prime-ideal {L} P {p} {q} = ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q ) |
149 | |
374 | 150 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where |
370 | 151 field |
374 | 152 filter : L → Set n |
371 | 153 f⊆P : PL filter |
374 | 154 filter1 : { p q : L } → PL (λ x → q ⊆ x ) → filter p → p ⊆ q → filter q |
371 | 155 filter2 : { p q : L } → filter p → filter q → filter (p ∩ q) |
156 | |
374 | 157 Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_ |
158 Filter-is-F {L} f = record { | |
159 filter = λ x → Lift (suc n) ((filter f) ∋ x) | |
160 ; f⊆P = λ x f∋x → power→⊆ _ _ (incl ( f⊆PL f ) (lower f∋x )) | |
161 ; filter1 = λ {p} {q} q⊆L f∋p p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q) | |
162 ; filter2 = λ {p} {q} f∋p f∋q → lift ( filter2 f (lower f∋p) (lower f∋q)) | |
163 } | |
164 | |
379 | 165 record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L → L → Set n) (_∩_ : L → L → L ) : Set (suc n) where |
166 field | |
167 dense : L → Set n | |
168 d⊆P : PL dense | |
169 dense-f : L → L | |
170 dense-d : { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p ) | |
171 dense-p : { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) | |
172 | |
173 Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_ | |
174 Dense-is-F {L} f = record { | |
175 dense = λ x → Lift (suc n) ((dense f) ∋ x) | |
176 ; d⊆P = λ x f∋x → power→⊆ _ _ (incl ( d⊆P f ) (lower f∋x )) | |
177 ; dense-f = λ x → dense-f f x | |
178 ; dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) ) | |
179 ; dense-p = λ {p} d → dense-p f (d p refl-⊆) | |
180 } where open Dense | |
181 | |
182 ------- | |
183 -- the set of finite partial functions from ω to 2 | |
184 -- | |
185 -- | |
186 | |
187 data Two : Set n where | |
188 i0 : Two | |
189 i1 : Two | |
190 | |
191 data Three : Set n where | |
192 j0 : Three | |
193 j1 : Three | |
194 j2 : Three | |
195 | |
196 open import Data.List hiding (map) | |
197 | |
198 import OPair | |
199 open OPair O | |
200 | |
201 record PFunc : Set (suc n) where | |
202 field | |
203 dom : Nat → Set n | |
204 map : (x : Nat ) → dom x → Two | |
205 meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q | |
206 | |
207 open PFunc | |
208 | |
209 data Findp : List Three → (x : Nat) → Set n where | |
210 v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero | |
211 v1 : {n : List Three} → Findp ( j1 ∷ n ) Zero | |
212 vn : {n : List Three} {d : Three} → {x : Nat} → Findp n x → Findp (d ∷ n) (Suc x) | |
213 | |
214 FPFunc→PFunc : List Three → PFunc | |
215 FPFunc→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → feq fp } where | |
216 findp : List Three → (x : Nat) → Set n | |
217 findp n x = Findp n x | |
218 find : (n : List Three ) → (x : Nat) → Findp n x → Two | |
219 find (j0 ∷ _) 0 v0 = i0 | |
220 find (j1 ∷ _) 0 v1 = i1 | |
221 find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p | |
222 feq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q | |
223 feq n {0} {v0} {v0} = refl | |
224 feq n {0} {v1} {v1} = refl | |
225 feq [] {Suc x} {()} | |
226 feq (_ ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) {!!} {!!} (feq n {x} {p} {q}) | |
227 | |
228 record _f⊆_ (f g : PFunc) : Set (suc n) where | |
229 field | |
230 extend : {x : Nat} → (fr : dom f x ) → dom g x | |
231 feq : {x : Nat} → {fr : dom f x } → map f x fr ≡ map g x (extend fr) | |
232 | |
233 open _f⊆_ | |
234 | |
374 | 235 min = Data.Nat._⊓_ |
236 -- m≤m⊔n = Data.Nat._⊔_ | |
237 open import Data.Nat.Properties | |
238 | |
375
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
239 _f∩_ : (f g : PFunc) → PFunc |
379 | 240 f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → map f x fr ≡ map g x gr) |
241 ; map = λ x p → map f x (proj1 p) ; meq = meq f } | |
375
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
242 |
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
243 _↑_ : (Nat → Two) → Nat → PFunc |
379 | 244 f ↑ i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl } |
375
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
245 |
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
246 record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where |
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
247 field |
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
248 gn : Nat |
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
249 f<n : (f ↑ gn) f⊆ p |
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
250 |
379 | 251 record FiniteF (p : PFunc ) : Set (suc n) where |
252 field | |
253 f-max : Nat | |
254 f-func : Nat → Two | |
255 f-p⊆f : p f⊆ (f-func ↑ f-max) | |
256 f-f⊆p : (f-func ↑ f-max) f⊆ p | |
257 | |
258 open FiniteF | |
259 | |
260 Dense-Gf : F-Dense PFunc (λ x → Lift (suc n) One) _f⊆_ _f∩_ | |
261 Dense-Gf = record { | |
262 dense = λ x → FiniteF x | |
263 ; d⊆P = lift OneObj | |
264 ; dense-f = λ x → record { dom = {!!} ; map = {!!} } | |
265 ; dense-d = λ {p} d → {!!} | |
266 ; dense-p = λ {p} d → {!!} | |
267 } | |
268 | |
375
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
269 open Gf |
8cade5f660bd
Select : (X : HOD ) → ((x : HOD ) → X ∋ x → Set n ) → HOD does not work
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
374
diff
changeset
|
270 |
374 | 271 GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_ |
371 | 272 GF f = record { |
372 | 273 filter = λ p → Gf f p |
374 | 274 ; f⊆P = lift OneObj |
275 ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q } | |
276 ; filter2 = λ {p} {q} fp fq → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq } | |
372 | 277 } where |
374 | 278 f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q |
379 | 279 f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q (extend (f<n fp ) x<g) ; feq = λ {x} {fr} → lemma {x} {fr} } where |
280 lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → map (f ↑ gn fp) x fr ≡ map q x (extend p⊆q (extend (f<n fp) fr)) | |
281 lemma {x} {fr} = begin | |
282 map (f ↑ gn fp) x fr | |
283 ≡⟨ feq (f<n fp ) ⟩ | |
284 map p x (extend (f<n fp) fr) | |
285 ≡⟨ feq p⊆q ⟩ | |
286 map q x (extend p⊆q (extend (f<n fp) fr)) | |
287 ∎ where open ≡-Reasoning | |
374 | 288 f2 : {p q : PFunc } → (fp : Gf f p ) → (fq : Gf f q ) → (f ↑ (min (gn fp) (gn fq))) f⊆ (p f∩ q) |
379 | 289 f2 {p} {q} fp fq = record { extend = λ {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where |
290 fmin = f ↑ (min (gn fp) (gn fq)) | |
291 lemma1 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p x) (gr : dom q x) → map p x fr ≡ map q x gr | |
292 lemma1 {x} x<g fr gr = begin | |
293 map p x fr | |
294 ≡⟨ meq p ⟩ | |
295 map p x (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))) | |
296 ≡⟨ sym (feq (f<n fp)) ⟩ | |
297 map (f ↑ (min (gn fp) (gn fq))) x x<g | |
298 ≡⟨ feq (f<n fq) ⟩ | |
299 map q x (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))) | |
300 ≡⟨ meq q ⟩ | |
301 map q x gr | |
302 ∎ where open ≡-Reasoning | |
303 lemma2 : {x : Nat} → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) x | |
304 lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ; | |
305 proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }} | |
306 f∩→⊆ : (p q : PFunc ) → (p f∩ q ) f⊆ q | |
307 f∩→⊆ p q = record { | |
308 extend = λ {x} pq → proj1 (proj2 pq) | |
309 ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) | |
310 } | |
311 lemma3 : {x : Nat} → ( fr : Lift n (x ≤ min (gn fp) (gn fq))) → map (f ↑ min (gn fp) (gn fq)) x fr ≡ map (p f∩ q) x (lemma2 fr) | |
312 lemma3 {x} fr = | |
313 map (f ↑ min (gn fp) (gn fq)) x fr | |
314 ≡⟨ feq (f<n fq) ⟩ | |
315 map q x (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) )) | |
316 ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} ) ⟩ | |
317 map (p f∩ q) x (lemma2 fr) | |
318 ∎ where open ≡-Reasoning | |
319 | |
370 | 320 |
363 | 321 ODSuc : (y : HOD) → infinite ∋ y → HOD |
322 ODSuc y lt = Union (y , (y , y)) | |
323 | |
366 | 324 data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where |
325 hφ : Hω2 0 o∅ | |
326 h0 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
327 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) , ord→od x ))) | |
328 h1 : {i : Nat} {x : Ordinal } → Hω2 i x → | |
329 Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) , ord→od x ))) | |
330 he : {i : Nat} {x : Ordinal } → Hω2 i x → | |
331 Hω2 (Suc i) x | |
332 | |
333 record Hω2r (x : Ordinal) : Set n where | |
334 field | |
335 count : Nat | |
336 hω2 : Hω2 count x | |
337 | |
338 open Hω2r | |
363 | 339 |
340 HODω2 : HOD | |
366 | 341 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where |
365 | 342 ω<next : {y : Ordinal} → infinite-d y → y o< next o∅ |
343 ω<next = ω<next-o∅ ho< | |
366 | 344 lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x |
345 lemma = {!!} | |
346 odmax0 : {y : Ordinal} → Hω2r y → y o< next o∅ | |
347 odmax0 {y} r with hω2 r | |
348 ... | hφ = x<nx | |
349 ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x}) | |
350 ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x}) | |
351 ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx | |
363 | 352 |
370 | 353 ω→2 : HOD |
379 | 354 ω→2 = Replace (Power infinite) (λ p → Replace infinite (λ x → < x , repl p x > )) where |
370 | 355 repl : HOD → HOD → HOD |
356 repl p x with ODC.∋-p O p x | |
357 ... | yes _ = nat→ω 1 | |
358 ... | no _ = nat→ω 0 | |
368 | 359 |
370 | 360 record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where |
361 -- field | |
362 -- n : HOD | |
363 -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n | |
364 | |
372 | 365 -- Gf : {f : HOD} → ω→2 ∋ f → HOD |
366 -- Gf {f} lt = Select HODω2 (λ x H∋x → {!!} ) | |
368 | 367 |
368 G : (Nat → Two) → Filter HODω2 | |
369 G f = record { | |
365 | 370 filter = {!!} |
371 ; f⊆PL = {!!} | |
372 ; filter1 = {!!} | |
373 ; filter2 = {!!} | |
374 } where | |
375 filter0 : HOD | |
376 filter0 = {!!} | |
377 f⊆PL1 : filter0 ⊆ Power HODω2 | |
378 f⊆PL1 = {!!} | |
379 filter11 : { p q : HOD } → q ⊆ HODω2 → filter0 ∋ p → p ⊆ q → filter0 ∋ q | |
380 filter11 = {!!} | |
381 filter12 : { p q : HOD } → filter0 ∋ p → filter0 ∋ q → filter0 ∋ (p ∩ q) | |
382 filter12 = {!!} | |
383 | |
363 | 384 -- the set of finite partial functions from ω to 2 |
385 | |
386 Hω2f : Set (suc n) | |
387 Hω2f = (Nat → Set n) → Two | |
388 | |
389 Hω2f→Hω2 : Hω2f → HOD | |
390 Hω2f→Hω2 p = record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} } | |
391 | |
392 |