|
1200
|
1 {-# OPTIONS --allow-unsolved-metas #-}
|
|
1244
|
2 import Level
|
|
431
|
3 open import Ordinals
|
|
1242
|
4 module generic-filter {n : Level.Level } (O : Ordinals {n}) where
|
|
431
|
5
|
|
1244
|
6 import filter
|
|
431
|
7 open import zf
|
|
|
8 open import logic
|
|
|
9 -- open import partfunc {n} O
|
|
1244
|
10 import OD
|
|
431
|
11
|
|
1244
|
12 open import Relation.Nullary
|
|
|
13 open import Relation.Binary
|
|
|
14 open import Data.Empty
|
|
431
|
15 open import Relation.Binary
|
|
|
16 open import Relation.Binary.Core
|
|
|
17 open import Relation.Binary.PropositionalEquality
|
|
1244
|
18 open import Data.Nat
|
|
|
19 import BAlgebra
|
|
431
|
20
|
|
1124
|
21 open BAlgebra O
|
|
431
|
22
|
|
|
23 open inOrdinal O
|
|
|
24 open OD O
|
|
|
25 open OD.OD
|
|
|
26 open ODAxiom odAxiom
|
|
|
27 import OrdUtil
|
|
|
28 import ODUtil
|
|
|
29 open Ordinals.Ordinals O
|
|
|
30 open Ordinals.IsOrdinals isOrdinal
|
|
|
31 open Ordinals.IsNext isNext
|
|
|
32 open OrdUtil O
|
|
|
33 open ODUtil O
|
|
|
34
|
|
|
35
|
|
|
36 import ODC
|
|
|
37
|
|
|
38 open filter O
|
|
|
39
|
|
|
40 open _∧_
|
|
|
41 open _∨_
|
|
|
42 open Bool
|
|
|
43
|
|
|
44
|
|
|
45 open HOD
|
|
|
46
|
|
|
47 -------
|
|
|
48 -- the set of finite partial functions from ω to 2
|
|
|
49 --
|
|
|
50 --
|
|
|
51
|
|
|
52 open import Data.List hiding (filter)
|
|
1244
|
53 open import Data.Maybe
|
|
431
|
54
|
|
1218
|
55 open import ZProduct O
|
|
431
|
56
|
|
1242
|
57 record CountableModel : Set (Level.suc (Level.suc n)) where
|
|
431
|
58 field
|
|
461
|
59 ctl-M : HOD
|
|
1242
|
60 ctl→ : ℕ → Ordinal
|
|
1244
|
61 ctl<M : (x : ℕ) → odef (ctl-M) (ctl→ x)
|
|
1242
|
62 ctl← : (x : Ordinal )→ odef (ctl-M ) x → ℕ
|
|
1244
|
63 ctl-iso→ : { x : Ordinal } → (lt : odef (ctl-M) x ) → ctl→ (ctl← x lt ) ≡ x
|
|
1174
|
64 -- we have no otherway round
|
|
1242
|
65 -- ctl-iso← : { x : ℕ } → ctl← (ctl→ x ) (ctl<M x) ≡ x
|
|
446
|
66 --
|
|
|
67 -- almmost universe
|
|
|
68 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
|
|
1244
|
69 --
|
|
436
|
70
|
|
1244
|
71 -- we expect P ∈ * ctl-M ∧ G ⊆ L ⊆ Power P , ¬ G ∈ * ctl-M,
|
|
434
|
72
|
|
1244
|
73 open CountableModel
|
|
431
|
74
|
|
|
75 ----
|
|
|
76 -- a(n) ∈ M
|
|
1239
|
77 -- ∃ q ∈ L ⊆ Power P → q ∈ a(n) ∧ p(n) ⊆ q
|
|
431
|
78 --
|
|
1242
|
79 PGHOD : (i : ℕ) (L : HOD) (C : CountableModel ) → (p : Ordinal) → HOD
|
|
457
|
80 PGHOD i L C p = record { od = record { def = λ x →
|
|
1239
|
81 odef L x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) }
|
|
1244
|
82 ; odmax = odmax L ; <odmax = λ {y} lt → <odmax L (proj1 lt) }
|
|
431
|
83
|
|
|
84 ---
|
|
1239
|
85 -- p(n+1) = if ({q | q ∈ a(n) ∧ p(n) ⊆ q)} != ∅ then q otherwise p(n)
|
|
1244
|
86 --
|
|
1242
|
87 find-p : (L : HOD ) (C : CountableModel ) (i : ℕ) → (x : Ordinal) → Ordinal
|
|
|
88 find-p L C zero x = x
|
|
|
89 find-p L C (suc i) x with is-o∅ ( & ( PGHOD i L C (find-p L C i x)) )
|
|
457
|
90 ... | yes y = find-p L C i x
|
|
|
91 ... | no not = & (ODC.minimal O ( PGHOD i L C (find-p L C i x)) (λ eq → not (=od∅→≡o∅ eq))) -- axiom of choice
|
|
431
|
92
|
|
|
93 ---
|
|
1239
|
94 -- G = { r ∈ L ⊆ Power P | ∃ n → r ⊆ p(n) }
|
|
431
|
95 --
|
|
457
|
96 record PDN (L p : HOD ) (C : CountableModel ) (x : Ordinal) : Set n where
|
|
431
|
97 field
|
|
1242
|
98 gr : ℕ
|
|
1244
|
99 pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p L C gr (& p))) y
|
|
457
|
100 x∈PP : odef L x
|
|
431
|
101
|
|
|
102 open PDN
|
|
|
103
|
|
|
104 ---
|
|
|
105 -- G as a HOD
|
|
|
106 --
|
|
457
|
107 PDHOD : (L p : HOD ) (C : CountableModel ) → HOD
|
|
|
108 PDHOD L p C = record { od = record { def = λ x → PDN L p C x }
|
|
1244
|
109 ; odmax = odmax L ; <odmax = λ {y} lt → <odmax L {y} (PDN.x∈PP lt) }
|
|
431
|
110
|
|
|
111 open PDN
|
|
|
112
|
|
|
113 ----
|
|
1242
|
114 -- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. ℕ → P → Set )
|
|
431
|
115 --
|
|
|
116 -- p 0 ≡ ∅
|
|
434
|
117 -- p (suc n) = if ∃ q ∈ M ∧ p n ⊆ q → q (by axiom of choice) ( q = * ( ctl→ n ) )
|
|
431
|
118 --- else p n
|
|
|
119
|
|
|
120 P∅ : {P : HOD} → odef (Power P) o∅
|
|
|
121 P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where
|
|
|
122 lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
|
|
|
123 lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt ))
|
|
|
124 x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
|
|
|
125 x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt
|
|
|
126
|
|
1242
|
127 gf05 : {a b : HOD} {x : Ordinal } → (odef (a ∪ b) x ) → ¬ odef a x → ¬ odef b x → ⊥
|
|
1244
|
128 gf05 {a} {b} {x} (case1 ax) nax nbx = nax ax
|
|
1242
|
129 gf05 {a} {b} {x} (case2 bx) nax nbx = nbx bx
|
|
|
130
|
|
|
131 gf02 : {P a b : HOD } → (P ＼ a) ∩ (P ＼ b) ≡ ( P ＼ (a ∪ b) )
|
|
|
132 gf02 {P} {a} {b} = ==→o≡ record { eq→ = gf03 ; eq← = gf04 }where
|
|
|
133 gf03 : {x : Ordinal} → odef ((P ＼ a) ∩ (P ＼ b)) x → odef (P ＼ (a ∪ b)) x
|
|
|
134 gf03 {x} ⟪ ⟪ Px , ¬ax ⟫ , ⟪ _ , ¬bx ⟫ ⟫ = ⟪ Px , (λ pab → gf05 {a} {b} {x} pab ¬ax ¬bx ) ⟫
|
|
|
135 gf04 : {x : Ordinal} → odef (P ＼ (a ∪ b)) x → odef ((P ＼ a) ∩ (P ＼ b)) x
|
|
1244
|
136 gf04 {x} ⟪ Px , abx ⟫ = ⟪ ⟪ Px , (λ ax → abx (case1 ax) ) ⟫ , ⟪ Px , (λ bx → abx (case2 bx) ) ⟫ ⟫
|
|
1242
|
137
|
|
446
|
138 open import Data.Nat.Properties
|
|
|
139 open import nat
|
|
433
|
140
|
|
1242
|
141 p-monotonic1 : (L p : HOD ) (C : CountableModel ) → {n : ℕ} → (* (find-p L C n (& p))) ⊆ (* (find-p L C (suc n) (& p)))
|
|
1096
|
142 p-monotonic1 L p C {n} {x} with is-o∅ (& (PGHOD n L C (find-p L C n (& p))))
|
|
|
143 ... | yes y = refl-⊆ {* (find-p L C n (& p))}
|
|
1242
|
144 ... | no not = λ lt → proj2 (proj2 fmin∈PGHOD) _ lt where
|
|
447
|
145 fmin : HOD
|
|
457
|
146 fmin = ODC.minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
147 fmin∈PGHOD : PGHOD n L C (find-p L C n (& p)) ∋ fmin
|
|
|
148 fmin∈PGHOD = ODC.x∋minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
|
|
438
|
149
|
|
1242
|
150 p-monotonic : (L p : HOD ) (C : CountableModel ) → {n m : ℕ} → n ≤ m → (* (find-p L C n (& p))) ⊆ (* (find-p L C m (& p)))
|
|
|
151 p-monotonic L p C {zero} {zero} n≤m = refl-⊆ {* (find-p L C zero (& p))}
|
|
|
152 p-monotonic L p C {zero} {suc m} z≤n lt = p-monotonic1 L p C {m} (p-monotonic L p C {zero} {m} z≤n lt )
|
|
|
153 p-monotonic L p C {suc n} {suc m} (s≤s n≤m) with <-cmp n m
|
|
1244
|
154 ... | tri< a ¬b ¬c = λ lt → p-monotonic1 L p C {m} (p-monotonic L p C {suc n} {m} a lt)
|
|
1096
|
155 ... | tri≈ ¬a refl ¬c = λ x → x
|
|
446
|
156 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
|
|
438
|
157
|
|
1242
|
158 record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (Level.suc n) where
|
|
1239
|
159 field
|
|
|
160 dense : HOD
|
|
|
161 d⊆P : dense ⊆ L
|
|
|
162 dense-f : {p : HOD} → L ∋ p → HOD
|
|
|
163 dense-d : { p : HOD} → (lt : L ∋ p) → dense ∋ dense-f lt
|
|
1245
|
164 dense-p : { p : HOD} → (lt : L ∋ p) → p ⊆ dense-f lt
|
|
1239
|
165
|
|
1242
|
166 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (Level.suc n) where
|
|
1239
|
167 field
|
|
|
168 genf : Filter {L} {P} LP
|
|
|
169 generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ Replace (Filter.filter genf) (λ x → P ＼ x )) ≡ od∅ )
|
|
|
170 rgen : HOD
|
|
|
171 rgen = Replace (Filter.filter genf) (λ x → P ＼ x )
|
|
|
172
|
|
1244
|
173 P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0
|
|
1245
|
174 → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) -- L is a Boolean Algebra
|
|
1244
|
175 → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q ))
|
|
1243
|
176 → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
|
|
1241
|
177 → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C )
|
|
1244
|
178 P-GenericFilter P L p0 L⊆PP Lp0 CAP UNI NEG C = record {
|
|
|
179 genf = record { filter = Replace (PDHOD L p0 C) (λ x → P ＼ x) ; f⊆L = gf01 ; filter1 = f1 ; filter2 = f2 }
|
|
1240
|
180 ; generic = λ D cd → subst (λ k → ¬ (Dense.dense D ∩ k) ≡ od∅ ) (sym gf00) (fdense D cd )
|
|
431
|
181 } where
|
|
1244
|
182 GP = Replace (PDHOD L p0 C) (λ x → P ＼ x)
|
|
|
183 f⊆PL : PDHOD L p0 C ⊆ L
|
|
|
184 f⊆PL lt = x∈PP lt
|
|
1241
|
185 gf01 : Replace (PDHOD L p0 C) (λ x → P ＼ x) ⊆ L
|
|
|
186 gf01 {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef L k) (sym x=ψz) ( NEG (subst (λ k → odef L k) (sym &iso) (f⊆PL az)) )
|
|
1242
|
187 gf141 : {xp xq : Ordinal } → (Pp : PDN L p0 C xp) (Pq : PDN L p0 C xq) → (* xp ∪ * xq) ⊆ P
|
|
|
188 gf141 Pp Pq {x} (case1 xpx) = L⊆PP (PDN.x∈PP Pp) _ xpx
|
|
|
189 gf141 Pp Pq {x} (case2 xqx) = L⊆PP (PDN.x∈PP Pq) _ xqx
|
|
|
190 gf121 : {p q : HOD} (gp : GP ∋ p) (gq : GP ∋ q) → p ∩ q ≡ P ＼ * (& (* (Replaced.z gp) ∪ * (Replaced.z gq)))
|
|
|
191 gf121 {p} {q} gp gq = begin
|
|
|
192 p ∩ q ≡⟨ cong₂ (λ j k → j ∩ k ) (sym *iso) (sym *iso) ⟩
|
|
|
193 (* (& p)) ∩ (* (& q)) ≡⟨ cong₂ (λ j k → ( * j ) ∩ ( * k)) (Replaced.x=ψz gp) (Replaced.x=ψz gq) ⟩
|
|
|
194 * (& (P ＼ (* xp ))) ∩ (* (& (P ＼ (* xq )))) ≡⟨ cong₂ (λ j k → j ∩ k ) *iso *iso ⟩
|
|
|
195 (P ＼ (* xp )) ∩ (P ＼ (* xq )) ≡⟨ gf02 {P} {* xp} {* xq} ⟩
|
|
|
196 P ＼ ((* xp) ∪ (* xq)) ≡⟨ cong (λ k → P ＼ k) (sym *iso) ⟩
|
|
1244
|
197 P ＼ * (& (* xp ∪ * xq)) ∎ where
|
|
1242
|
198 open ≡-Reasoning
|
|
|
199 xp = Replaced.z gp
|
|
|
200 xq = Replaced.z gq
|
|
|
201 gf131 : {p q : HOD} (gp : GP ∋ p) (gq : GP ∋ q) → P ＼ (p ∩ q) ≡ * (Replaced.z gp) ∪ * (Replaced.z gq)
|
|
|
202 gf131 {p} {q} gp gq = trans (cong (λ k → P ＼ k) (gf121 gp gq))
|
|
|
203 (trans ( L＼Lx=x (subst (λ k → k ⊆ P) (sym *iso) (gf141 (Replaced.az gp) (Replaced.az gq))) ) *iso )
|
|
|
204
|
|
1244
|
205 f1 : {p q : HOD} → L ∋ q → Replace (PDHOD L p0 C) (λ x → P ＼ x) ∋ p → p ⊆ q → Replace (PDHOD L p0 C) (λ x → P ＼ x) ∋ q
|
|
|
206 f1 {p} {q} L∋q record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = _
|
|
|
207 ; az = record { gr = gr az ; pn<gr = f04 ; x∈PP = NEG L∋q } ; x=ψz = f05 } where
|
|
|
208 open ≡-Reasoning
|
|
|
209 f04 : (y : Ordinal) → odef (* (& (P ＼ q))) y → odef (* (find-p L C (gr az ) (& p0))) y
|
|
|
210 f04 y qy = PDN.pn<gr az _ (subst (λ k → odef k y ) f06 (f03 qy )) where
|
|
|
211 f06 : * (& (P ＼ p)) ≡ * z
|
|
|
212 f06 = begin
|
|
|
213 * (& (P ＼ p)) ≡⟨ *iso ⟩
|
|
|
214 P ＼ p ≡⟨ cong (λ k → P ＼ k) (sym *iso) ⟩
|
|
|
215 P ＼ (* (& p)) ≡⟨ cong (λ k → P ＼ k) (cong (*) x=ψz) ⟩
|
|
|
216 P ＼ (* (& (P ＼ * z))) ≡⟨ cong ( λ k → P ＼ k) *iso ⟩
|
|
|
217 P ＼ (P ＼ * z) ≡⟨ L＼Lx=x (λ {x} lt → L⊆PP (x∈PP az) _ lt ) ⟩
|
|
|
218 * z ∎
|
|
|
219 f03 : odef (* (& (P ＼ q))) y → odef (* (& (P ＼ p))) y
|
|
|
220 f03 pqy with subst (λ k → odef k y ) *iso pqy
|
|
|
221 ... | ⟪ Py , nqy ⟫ = subst (λ k → odef k y ) (sym *iso) ⟪ Py , (λ py → nqy (p⊆q py) ) ⟫
|
|
|
222 f05 : & q ≡ & (P ＼ * (& (P ＼ q)))
|
|
|
223 f05 = cong (&) ( begin
|
|
|
224 q ≡⟨ sym (L＼Lx=x (λ {x} lt → L⊆PP L∋q _ (subst (λ k → odef k x) (sym *iso) lt) )) ⟩
|
|
|
225 P ＼ (P ＼ q ) ≡⟨ cong ( λ k → P ＼ k) (sym *iso) ⟩
|
|
|
226 P ＼ * (& (P ＼ q)) ∎ )
|
|
1241
|
227 f2 : {p q : HOD} → GP ∋ p → GP ∋ q → L ∋ (p ∩ q) → GP ∋ (p ∩ q)
|
|
1244
|
228 f2 {p} {q} record { z = xp ; az = Pp ; x=ψz = peq }
|
|
|
229 record { z = xq ; az = Pq ; x=ψz = qeq } L∋pq with <-cmp (gr Pp) (gr Pq)
|
|
1242
|
230 ... | tri< a ¬b ¬c = record { z = & ( (* xp) ∪ (* xq) ) ; az = gf10 ; x=ψz = cong (&) (gf121 gp gq) } where
|
|
1244
|
231 gp = record { z = xp ; az = Pp ; x=ψz = peq }
|
|
|
232 gq = record { z = xq ; az = Pq ; x=ψz = qeq }
|
|
1242
|
233 gf10 : odef (PDHOD L p0 C) (& (* xp ∪ * xq))
|
|
|
234 gf10 = record { gr = PDN.gr Pq ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ( NEG L∋pq ) } where
|
|
|
235 gf16 : gr Pp ≤ gr Pq
|
|
|
236 gf16 = <to≤ a
|
|
|
237 gf15 : (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pq) (& p0))) y
|
|
1244
|
238 gf15 y gpqy with subst (λ k → odef k y ) *iso gpqy
|
|
1242
|
239 ... | case1 xpy = p-monotonic L p0 C gf16 (PDN.pn<gr Pp y xpy )
|
|
|
240 ... | case2 xqy = PDN.pn<gr Pq _ xqy
|
|
1244
|
241 ... | tri≈ ¬a eq ¬c = record { z = & (* xp ∪ * xq) ; az = record { gr = gr Pp ; pn<gr = gf21 ; x∈PP = gf22 } ; x=ψz = gf23 } where
|
|
|
242 gp = record { z = xp ; az = Pp ; x=ψz = peq }
|
|
|
243 gq = record { z = xq ; az = Pq ; x=ψz = qeq }
|
|
|
244 gf22 : odef L (& (* xp ∪ * xq))
|
|
|
245 gf22 = UNI (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pp)) (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pq))
|
|
|
246 gf21 : (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pp) (& p0))) y
|
|
1243
|
247 gf21 y xpqy with subst (λ k → odef k y) *iso xpqy
|
|
1244
|
248 ... | case1 xpy = PDN.pn<gr Pp _ xpy
|
|
|
249 ... | case2 xqy = subst (λ k → odef (* (find-p L C k (& p0))) y ) (sym eq) ( PDN.pn<gr Pq _ xqy )
|
|
1243
|
250 gf25 : odef L (& p)
|
|
|
251 gf25 = subst (λ k → odef L k ) (sym peq) ( NEG (subst (λ k → odef L k) (sym &iso) (PDN.x∈PP Pp) ))
|
|
|
252 gf27 : {x : Ordinal} → odef p x → odef (P ＼ * xp) x
|
|
|
253 gf27 {x} px = subst (λ k → odef k x) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) peq)) px
|
|
1244
|
254 -- gf02 : {P a b : HOD } → (P ＼ a) ∩ (P ＼ b) ≡ ( P ＼ (a ∪ b) )
|
|
|
255 gf23 : & (p ∩ q) ≡ & (P ＼ * (& (* xp ∪ * xq)))
|
|
|
256 gf23 = cong (&) (gf121 gp gq )
|
|
|
257 ... | tri> ¬a ¬b c = record { z = & ( (* xp) ∪ (* xq) ) ; az = gf10 ; x=ψz = cong (&) (gf121 gp gq ) } where
|
|
|
258 gp = record { z = xp ; az = Pp ; x=ψz = peq }
|
|
|
259 gq = record { z = xq ; az = Pq ; x=ψz = qeq }
|
|
1242
|
260 gf10 : odef (PDHOD L p0 C) (& (* xp ∪ * xq))
|
|
|
261 gf10 = record { gr = PDN.gr Pp ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ( NEG L∋pq ) } where
|
|
|
262 gf16 : gr Pq ≤ gr Pp
|
|
|
263 gf16 = <to≤ c
|
|
|
264 gf15 : (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pp) (& p0))) y
|
|
1244
|
265 gf15 y gpqy with subst (λ k → odef k y ) *iso gpqy
|
|
1242
|
266 ... | case1 xpy = PDN.pn<gr Pp _ xpy
|
|
|
267 ... | case2 xqy = p-monotonic L p0 C gf16 (PDN.pn<gr Pq y xqy )
|
|
1240
|
268 gf00 : Replace (Replace (PDHOD L p0 C) (λ x → P ＼ x)) (_＼_ P) ≡ PDHOD L p0 C
|
|
1242
|
269 gf00 = ==→o≡ record { eq→ = gf20 ; eq← = gf22 } where
|
|
|
270 gf20 : {x : Ordinal} → odef (Replace (Replace (PDHOD L p0 C) (λ x₁ → P ＼ x₁)) (_＼_ P)) x → PDN L p0 C x
|
|
1244
|
271 gf20 {x} record { z = z₁ ; az = record { z = z ; az = az ; x=ψz = x=ψz₁ } ; x=ψz = x=ψz } =
|
|
1242
|
272 subst (λ k → PDN L p0 C k ) (begin
|
|
1244
|
273 z ≡⟨ sym &iso ⟩
|
|
|
274 & (* z) ≡⟨ cong (&) (sym (L＼Lx=x gf21 )) ⟩
|
|
|
275 & (P ＼ ( P ＼ (* z) )) ≡⟨ cong (λ k → & ( P ＼ k)) (sym *iso) ⟩
|
|
|
276 & (P ＼ (* ( & (P ＼ (* z ))))) ≡⟨ cong (λ k → & (P ＼ (* k))) (sym x=ψz₁) ⟩
|
|
|
277 & (P ＼ (* z₁)) ≡⟨ sym x=ψz ⟩
|
|
|
278 x ∎ ) az where
|
|
1242
|
279 open ≡-Reasoning
|
|
|
280 gf21 : {x : Ordinal } → odef (* z) x → odef P x
|
|
1244
|
281 gf21 {x} lt = L⊆PP ( PDN.x∈PP az) _ lt
|
|
|
282 gf22 : {x : Ordinal} → PDN L p0 C x → odef (Replace (Replace (PDHOD L p0 C) (λ x₁ → P ＼ x₁)) (_＼_ P)) x
|
|
1242
|
283 gf22 {x} pdx = record { z = _ ; az = record { z = _ ; az = pdx ; x=ψz = refl } ; x=ψz = ( begin
|
|
1244
|
284 x ≡⟨ sym &iso ⟩
|
|
|
285 & (* x) ≡⟨ cong (&) (sym (L＼Lx=x gf21 )) ⟩
|
|
|
286 & (P ＼ (P ＼ * x)) ≡⟨ cong (λ k → & ( P ＼ k)) (sym *iso) ⟩
|
|
|
287 & (P ＼ * (& (P ＼ * x))) ∎ ) } where
|
|
1242
|
288 open ≡-Reasoning
|
|
|
289 gf21 : {z : Ordinal } → odef (* x) z → odef P z
|
|
|
290 gf21 {z} lt = L⊆PP ( PDN.x∈PP pdx ) z lt
|
|
1240
|
291 fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D → ¬ (Dense.dense D ∩ (PDHOD L p0 C)) ≡ od∅
|
|
1245
|
292 fdense D MD eq0 = ⊥-elim ( ∅< {Dense.dense D ∩ PDHOD L p0 C} fd01 (≡od∅→=od∅ eq0 )) where
|
|
448
|
293 open Dense
|
|
1245
|
294 fd09 : (i : ℕ ) → odef L (find-p L C i (& p0))
|
|
|
295 fd09 zero = Lp0
|
|
|
296 fd09 (suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) )
|
|
|
297 ... | yes _ = fd09 i
|
|
|
298 ... | no not = fd17 where
|
|
|
299 fd19 = ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
300 fd18 : PGHOD i L C (find-p L C i (& p0)) ∋ fd19
|
|
|
301 fd18 = ODC.x∋minimal O (PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
302 fd17 : odef L ( & (ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))) )
|
|
|
303 fd17 = proj1 fd18
|
|
|
304 an : ℕ
|
|
|
305 an = ctl← C (& (dense D)) MD
|
|
|
306 pn : Ordinal
|
|
|
307 pn = find-p L C an (& p0)
|
|
|
308 pn+1 : Ordinal
|
|
|
309 pn+1 = find-p L C (suc an) (& p0)
|
|
|
310 d=an : dense D ≡ * (ctl→ C an)
|
|
|
311 d=an = begin dense D ≡⟨ sym *iso ⟩
|
|
|
312 * ( & (dense D)) ≡⟨ cong (*) (sym (ctl-iso→ C MD )) ⟩
|
|
|
313 * (ctl→ C an) ∎ where open ≡-Reasoning
|
|
|
314 fd07 : odef (dense D) pn+1
|
|
|
315 fd07 with is-o∅ ( & ( PGHOD an L C (find-p L C an (& p0))) )
|
|
|
316 ... | yes y = ⊥-elim ( ¬x<0 ( _==_.eq→ fd10 fd21 ) ) where
|
|
|
317 L∋pn : L ∋ * (find-p L C an (& p0))
|
|
|
318 L∋pn = subst (λ k → odef L k) (sym &iso) (fd09 an )
|
|
|
319 L∋df : L ∋ ( dense-f D L∋pn )
|
|
|
320 L∋df = (d⊆P D) ( dense-d D L∋pn )
|
|
|
321 pn∋df : (* (ctl→ C an)) ∋ ( dense-f D L∋pn )
|
|
|
322 pn∋df = subst (λ k → odef k (& ( dense-f D L∋pn ) )) d=an ( dense-d D L∋pn )
|
|
|
323 pn⊆df : (y : Ordinal) → odef (* (find-p L C an (& p0))) y → odef (* (& (dense-f D L∋pn))) y
|
|
|
324 pn⊆df y py = subst (λ k → odef k y ) (sym *iso) (dense-p D L∋pn py)
|
|
|
325 fd21 : odef (PGHOD an L C (find-p L C an (& p0)) ) (& (dense-f D L∋pn))
|
|
|
326 fd21 = ⟪ L∋df , ⟪ pn∋df , pn⊆df ⟫ ⟫
|
|
|
327 fd10 : PGHOD an L C (find-p L C an (& p0)) =h= od∅
|
|
|
328 fd10 = ≡o∅→=od∅ y
|
|
|
329 ... | no not = fd27 where
|
|
|
330 fd29 = ODC.minimal O ( PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
331 fd28 : PGHOD an L C (find-p L C an (& p0)) ∋ fd29
|
|
|
332 fd28 = ODC.x∋minimal O (PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
333 fd27 : odef (dense D) (& fd29)
|
|
|
334 fd27 = subst (λ k → odef k (& fd29)) (sym d=an) (proj1 (proj2 fd28))
|
|
|
335 fd03 : odef (PDHOD L p0 C) pn+1
|
|
|
336 fd03 = record { gr = suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (suc an)}
|
|
|
337 fd01 : (dense D ∩ PDHOD L p0 C) ∋ (* pn+1)
|
|
|
338 fd01 = ⟪ subst (λ k → odef (dense D) k ) (sym &iso) fd07 , subst (λ k → odef (PDHOD L p0 C) k) (sym &iso) fd03 ⟫
|
|
|
339
|
|
448
|
340
|
|
431
|
341 open GenericFilter
|
|
|
342 open Filter
|
|
|
343
|
|
1245
|
344 record NotCompatible (L p : HOD ) (L∋a : L ∋ p ) : Set (Level.suc (Level.suc n)) where
|
|
431
|
345 field
|
|
1245
|
346 q r : HOD
|
|
|
347 Lq : L ∋ q
|
|
|
348 Lr : L ∋ r
|
|
|
349 p⊆q : p ⊆ q
|
|
|
350 p⊆r : p ⊆ r
|
|
|
351 ¬compat : (s : HOD) → ¬ ( (q ⊆ s) ∧ (r ⊆ s) )
|
|
431
|
352
|
|
1246
|
353 lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
|
|
1245
|
354 → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) -- L is a Boolean Algebra
|
|
|
355 → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q ))
|
|
|
356 → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
|
|
|
357 → (C : CountableModel )
|
|
|
358 → ( MP : ctl-M C ∋ P )
|
|
|
359 → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp )
|
|
1246
|
360 → ¬ ( ctl-M C ∋ rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG C ))
|
|
|
361 lemma232 P L p0 LPP Lp0 CAP UNI NEG C MP NC M∋gf = ¬gf∩D=0 record { eq→ = λ {x} gf∩D → ⊥-elim( proj2 (proj2 gf∩D) (proj1 gf∩D))
|
|
1245
|
362 ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
|
|
1246
|
363 gf = rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG C )
|
|
1245
|
364 M = ctl-M C
|
|
|
365 D : HOD
|
|
|
366 D = L ＼ gf
|
|
|
367 M∋D : M ∋ D
|
|
|
368 M∋D = ?
|
|
1246
|
369 D⊆PP : D ⊆ Power P
|
|
|
370 D⊆PP {x} ⟪ Lx , ngx ⟫ = LPP Lx
|
|
|
371 DD : Dense {L} {P} LPP
|
|
|
372 Dense.dense DD = D
|
|
|
373 Dense.d⊆P DD ⟪ Lx , _ ⟫ = Lx
|
|
|
374 Dense.dense-f DD Lp = ? where
|
|
|
375 ll00 : HOD
|
|
|
376 ll00 with NotCompatible.¬compat (NC Lp)
|
|
|
377 ... | nc = ? where
|
|
|
378 ll01 : {q r : HOD } → (s : HOD) → ¬ ( (q ⊆ s) ∧ (r ⊆ s)) → (¬ (gf ∋ q)) ∨ (¬ (gf ∋ q))
|
|
|
379 ll01 = ?
|
|
|
380 Dense.dense-d DD = ?
|
|
|
381 Dense.dense-p DD = ?
|
|
1245
|
382 ¬gf∩D=0 : ¬ ( (gf ∩ D) =h= od∅ )
|
|
|
383 ¬gf∩D=0 = ?
|
|
431
|
384
|
|
|
385 --
|
|
1174
|
386 -- P-Generic Filter defines a countable model D ⊂ C from P
|
|
|
387 --
|
|
|
388
|
|
|
389 --
|
|
|
390 -- in D, we have V ≠ L
|
|
|
391 --
|
|
|
392
|
|
|
393 --
|
|
431
|
394 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
|
|
|
395 --
|
|
436
|
396
|
|
1242
|
397 record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (C : CountableModel ) (G : GenericFilter {L} {P} LP (ctl-M C) ) : Set (Level.suc n) where
|
|
437
|
398 field
|
|
|
399 valx : HOD
|
|
436
|
400
|
|
437
|
401 record valS (ox oy oG : Ordinal) : Set n where
|
|
436
|
402 field
|
|
437
|
403 op : Ordinal
|
|
1244
|
404 p∈G : odef (* oG) op
|
|
437
|
405 is-val : odef (* ox) ( & < * oy , * op > )
|
|
436
|
406
|
|
459
|
407 val : (x : HOD) {P L : HOD } {LP : L ⊆ Power P}
|
|
1096
|
408 → (G : GenericFilter {L} {P} LP {!!} )
|
|
436
|
409 → HOD
|
|
437
|
410 val x G = TransFinite {λ x → HOD } ind (& x) where
|
|
|
411 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
|
|
439
|
412 ind x valy = record { od = record { def = λ y → valS x y (& (filter (genf G))) } ; odmax = {!!} ; <odmax = {!!} }
|
|
437
|
413
|
