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