|
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) )
|
|
1250
|
134 gf02 {P} {a} {b} = ==→o≡ record { eq→ = gf03 ; eq← = gf04 } where
|
|
1242
|
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
|
|
1250
|
140 gf45 : {P a b : HOD } → (P ＼ a) ∪ (P ＼ b) ≡ ( P ＼ (a ∩ b) )
|
|
|
141 gf45 {P} {a} {b} = ==→o≡ record { eq→ = gf03 ; eq← = gf04 } where
|
|
|
142 gf03 : {x : Ordinal} → odef ((P ＼ a) ∪ (P ＼ b)) x → odef (P ＼ (a ∩ b)) x
|
|
|
143 gf03 {x} (case1 pa) = ⟪ proj1 pa , (λ ab → proj2 pa (proj1 ab) ) ⟫
|
|
|
144 gf03 {x} (case2 pb) = ⟪ proj1 pb , (λ ab → proj2 pb (proj2 ab) ) ⟫
|
|
|
145 gf04 : {x : Ordinal} → odef (P ＼ (a ∩ b)) x → odef ((P ＼ a) ∪ (P ＼ b)) x
|
|
|
146 gf04 {x} ⟪ Px , nab ⟫ with ODC.p∨¬p O (odef b x)
|
|
|
147 ... | case1 bx = case1 ⟪ Px , ( λ ax → nab ⟪ ax , bx ⟫ ) ⟫
|
|
|
148 ... | case2 nbx = case2 ⟪ Px , ( λ bx → nbx bx ) ⟫
|
|
|
149
|
|
446
|
150 open import Data.Nat.Properties
|
|
|
151 open import nat
|
|
433
|
152
|
|
1242
|
153 p-monotonic1 : (L p : HOD ) (C : CountableModel ) → {n : ℕ} → (* (find-p L C n (& p))) ⊆ (* (find-p L C (suc n) (& p)))
|
|
1096
|
154 p-monotonic1 L p C {n} {x} with is-o∅ (& (PGHOD n L C (find-p L C n (& p))))
|
|
|
155 ... | yes y = refl-⊆ {* (find-p L C n (& p))}
|
|
1242
|
156 ... | no not = λ lt → proj2 (proj2 fmin∈PGHOD) _ lt where
|
|
447
|
157 fmin : HOD
|
|
457
|
158 fmin = ODC.minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
159 fmin∈PGHOD : PGHOD n L C (find-p L C n (& p)) ∋ fmin
|
|
|
160 fmin∈PGHOD = ODC.x∋minimal O (PGHOD n L C (find-p L C n (& p))) (λ eq → not (=od∅→≡o∅ eq))
|
|
438
|
161
|
|
1242
|
162 p-monotonic : (L p : HOD ) (C : CountableModel ) → {n m : ℕ} → n ≤ m → (* (find-p L C n (& p))) ⊆ (* (find-p L C m (& p)))
|
|
|
163 p-monotonic L p C {zero} {zero} n≤m = refl-⊆ {* (find-p L C zero (& p))}
|
|
|
164 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 )
|
|
|
165 p-monotonic L p C {suc n} {suc m} (s≤s n≤m) with <-cmp n m
|
|
1244
|
166 ... | tri< a ¬b ¬c = λ lt → p-monotonic1 L p C {m} (p-monotonic L p C {suc n} {m} a lt)
|
|
1096
|
167 ... | tri≈ ¬a refl ¬c = λ x → x
|
|
446
|
168 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
|
|
438
|
169
|
|
1254
|
170 record Expansion (L : HOD) {p : HOD } (dense : HOD) (Lp : L ∋ p) : Set (Level.suc n) where
|
|
|
171 field
|
|
|
172 expansion : HOD
|
|
|
173 dense∋exp : dense ∋ expansion
|
|
|
174 p⊆exp : p ⊆ expansion
|
|
|
175
|
|
1242
|
176 record Dense {L P : HOD } (LP : L ⊆ Power P) : Set (Level.suc n) where
|
|
1239
|
177 field
|
|
|
178 dense : HOD
|
|
|
179 d⊆P : dense ⊆ L
|
|
1254
|
180 has-expansion : {p : HOD} → (Lp : L ∋ p) → Expansion L dense Lp
|
|
1239
|
181
|
|
1242
|
182 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (Level.suc n) where
|
|
1239
|
183 field
|
|
|
184 genf : Filter {L} {P} LP
|
|
|
185 rgen : HOD
|
|
|
186 rgen = Replace (Filter.filter genf) (λ x → P ＼ x )
|
|
1248
|
187 field
|
|
1254
|
188 generic : (D : Dense {L} {P} LP ) → M ∋ Dense.dense D → ¬ ( (Dense.dense D ∩ rgen ) ≡ od∅ )
|
|
|
189 gideal1 : {p q : HOD} → rgen ∋ p → q ⊆ p → L ∋ ( P ＼ q) → rgen ∋ q
|
|
|
190 gideal2 : {p q : HOD} → (rgen ∋ p ) ∧ (rgen ∋ q) → rgen ∋ (p ∪ q)
|
|
1239
|
191
|
|
1244
|
192 P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0
|
|
1245
|
193 → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) -- L is a Boolean Algebra
|
|
1244
|
194 → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q ))
|
|
1243
|
195 → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
|
|
1241
|
196 → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C )
|
|
1244
|
197 P-GenericFilter P L p0 L⊆PP Lp0 CAP UNI NEG C = record {
|
|
|
198 genf = record { filter = Replace (PDHOD L p0 C) (λ x → P ＼ x) ; f⊆L = gf01 ; filter1 = f1 ; filter2 = f2 }
|
|
1240
|
199 ; generic = λ D cd → subst (λ k → ¬ (Dense.dense D ∩ k) ≡ od∅ ) (sym gf00) (fdense D cd )
|
|
1254
|
200 ; gideal1 = gideal1
|
|
|
201 ; gideal2 = gideal2
|
|
431
|
202 } where
|
|
1248
|
203 GP = Replace (PDHOD L p0 C) (λ x → P ＼ x)
|
|
|
204 GPR = Replace GP (_＼_ P)
|
|
|
205 f⊆PL : PDHOD L p0 C ⊆ L
|
|
|
206 f⊆PL lt = x∈PP lt
|
|
|
207 gf01 : Replace (PDHOD L p0 C) (λ x → P ＼ x) ⊆ L
|
|
|
208 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)) )
|
|
|
209 gf141 : {xp xq : Ordinal } → (Pp : PDN L p0 C xp) (Pq : PDN L p0 C xq) → (* xp ∪ * xq) ⊆ P
|
|
|
210 gf141 Pp Pq {x} (case1 xpx) = L⊆PP (PDN.x∈PP Pp) _ xpx
|
|
|
211 gf141 Pp Pq {x} (case2 xqx) = L⊆PP (PDN.x∈PP Pq) _ xqx
|
|
|
212 gf121 : {p q : HOD} (gp : GP ∋ p) (gq : GP ∋ q) → p ∩ q ≡ P ＼ * (& (* (Replaced.z gp) ∪ * (Replaced.z gq)))
|
|
|
213 gf121 {p} {q} gp gq = begin
|
|
|
214 p ∩ q ≡⟨ cong₂ (λ j k → j ∩ k ) (sym *iso) (sym *iso) ⟩
|
|
|
215 (* (& p)) ∩ (* (& q)) ≡⟨ cong₂ (λ j k → ( * j ) ∩ ( * k)) (Replaced.x=ψz gp) (Replaced.x=ψz gq) ⟩
|
|
|
216 * (& (P ＼ (* xp ))) ∩ (* (& (P ＼ (* xq )))) ≡⟨ cong₂ (λ j k → j ∩ k ) *iso *iso ⟩
|
|
|
217 (P ＼ (* xp )) ∩ (P ＼ (* xq )) ≡⟨ gf02 {P} {* xp} {* xq} ⟩
|
|
|
218 P ＼ ((* xp) ∪ (* xq)) ≡⟨ cong (λ k → P ＼ k) (sym *iso) ⟩
|
|
|
219 P ＼ * (& (* xp ∪ * xq)) ∎ where
|
|
|
220 open ≡-Reasoning
|
|
|
221 xp = Replaced.z gp
|
|
|
222 xq = Replaced.z gq
|
|
|
223 gf131 : {p q : HOD} (gp : GP ∋ p) (gq : GP ∋ q) → P ＼ (p ∩ q) ≡ * (Replaced.z gp) ∪ * (Replaced.z gq)
|
|
|
224 gf131 {p} {q} gp gq = trans (cong (λ k → P ＼ k) (gf121 gp gq))
|
|
|
225 (trans ( L＼Lx=x (subst (λ k → k ⊆ P) (sym *iso) (gf141 (Replaced.az gp) (Replaced.az gq))) ) *iso )
|
|
1242
|
226
|
|
1248
|
227 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
|
|
|
228 f1 {p} {q} L∋q record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = _
|
|
|
229 ; az = record { gr = gr az ; pn<gr = f04 ; x∈PP = NEG L∋q } ; x=ψz = f05 } where
|
|
|
230 open ≡-Reasoning
|
|
|
231 f04 : (y : Ordinal) → odef (* (& (P ＼ q))) y → odef (* (find-p L C (gr az ) (& p0))) y
|
|
|
232 f04 y qy = PDN.pn<gr az _ (subst (λ k → odef k y ) f06 (f03 qy )) where
|
|
|
233 f06 : * (& (P ＼ p)) ≡ * z
|
|
|
234 f06 = begin
|
|
|
235 * (& (P ＼ p)) ≡⟨ *iso ⟩
|
|
|
236 P ＼ p ≡⟨ cong (λ k → P ＼ k) (sym *iso) ⟩
|
|
|
237 P ＼ (* (& p)) ≡⟨ cong (λ k → P ＼ k) (cong (*) x=ψz) ⟩
|
|
|
238 P ＼ (* (& (P ＼ * z))) ≡⟨ cong ( λ k → P ＼ k) *iso ⟩
|
|
|
239 P ＼ (P ＼ * z) ≡⟨ L＼Lx=x (λ {x} lt → L⊆PP (x∈PP az) _ lt ) ⟩
|
|
|
240 * z ∎
|
|
|
241 f03 : odef (* (& (P ＼ q))) y → odef (* (& (P ＼ p))) y
|
|
|
242 f03 pqy with subst (λ k → odef k y ) *iso pqy
|
|
|
243 ... | ⟪ Py , nqy ⟫ = subst (λ k → odef k y ) (sym *iso) ⟪ Py , (λ py → nqy (p⊆q py) ) ⟫
|
|
|
244 f05 : & q ≡ & (P ＼ * (& (P ＼ q)))
|
|
|
245 f05 = cong (&) ( begin
|
|
|
246 q ≡⟨ sym (L＼Lx=x (λ {x} lt → L⊆PP L∋q _ (subst (λ k → odef k x) (sym *iso) lt) )) ⟩
|
|
|
247 P ＼ (P ＼ q ) ≡⟨ cong ( λ k → P ＼ k) (sym *iso) ⟩
|
|
|
248 P ＼ * (& (P ＼ q)) ∎ )
|
|
|
249 f2 : {p q : HOD} → GP ∋ p → GP ∋ q → L ∋ (p ∩ q) → GP ∋ (p ∩ q)
|
|
|
250 f2 {p} {q} record { z = xp ; az = Pp ; x=ψz = peq }
|
|
|
251 record { z = xq ; az = Pq ; x=ψz = qeq } L∋pq with <-cmp (gr Pp) (gr Pq)
|
|
|
252 ... | tri< a ¬b ¬c = record { z = & ( (* xp) ∪ (* xq) ) ; az = gf10 ; x=ψz = cong (&) (gf121 gp gq) } where
|
|
|
253 gp = record { z = xp ; az = Pp ; x=ψz = peq }
|
|
|
254 gq = record { z = xq ; az = Pq ; x=ψz = qeq }
|
|
|
255 gf10 : odef (PDHOD L p0 C) (& (* xp ∪ * xq))
|
|
|
256 gf10 = record { gr = PDN.gr Pq ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ( NEG L∋pq ) } where
|
|
|
257 gf16 : gr Pp ≤ gr Pq
|
|
|
258 gf16 = <to≤ a
|
|
|
259 gf15 : (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pq) (& p0))) y
|
|
|
260 gf15 y gpqy with subst (λ k → odef k y ) *iso gpqy
|
|
|
261 ... | case1 xpy = p-monotonic L p0 C gf16 (PDN.pn<gr Pp y xpy )
|
|
|
262 ... | case2 xqy = PDN.pn<gr Pq _ xqy
|
|
|
263 ... | tri≈ ¬a eq ¬c = record { z = & (* xp ∪ * xq) ; az = record { gr = gr Pp ; pn<gr = gf21 ; x∈PP = gf22 } ; x=ψz = gf23 } where
|
|
|
264 gp = record { z = xp ; az = Pp ; x=ψz = peq }
|
|
|
265 gq = record { z = xq ; az = Pq ; x=ψz = qeq }
|
|
|
266 gf22 : odef L (& (* xp ∪ * xq))
|
|
|
267 gf22 = UNI (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pp)) (subst (λ k → odef L k ) (sym &iso) (PDN.x∈PP Pq))
|
|
|
268 gf21 : (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pp) (& p0))) y
|
|
|
269 gf21 y xpqy with subst (λ k → odef k y) *iso xpqy
|
|
|
270 ... | case1 xpy = PDN.pn<gr Pp _ xpy
|
|
|
271 ... | case2 xqy = subst (λ k → odef (* (find-p L C k (& p0))) y ) (sym eq) ( PDN.pn<gr Pq _ xqy )
|
|
|
272 gf25 : odef L (& p)
|
|
|
273 gf25 = subst (λ k → odef L k ) (sym peq) ( NEG (subst (λ k → odef L k) (sym &iso) (PDN.x∈PP Pp) ))
|
|
|
274 gf27 : {x : Ordinal} → odef p x → odef (P ＼ * xp) x
|
|
|
275 gf27 {x} px = subst (λ k → odef k x) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) peq)) px
|
|
|
276 -- gf02 : {P a b : HOD } → (P ＼ a) ∩ (P ＼ b) ≡ ( P ＼ (a ∪ b) )
|
|
|
277 gf23 : & (p ∩ q) ≡ & (P ＼ * (& (* xp ∪ * xq)))
|
|
|
278 gf23 = cong (&) (gf121 gp gq )
|
|
|
279 ... | tri> ¬a ¬b c = record { z = & ( (* xp) ∪ (* xq) ) ; az = gf10 ; x=ψz = cong (&) (gf121 gp gq ) } where
|
|
|
280 gp = record { z = xp ; az = Pp ; x=ψz = peq }
|
|
|
281 gq = record { z = xq ; az = Pq ; x=ψz = qeq }
|
|
|
282 gf10 : odef (PDHOD L p0 C) (& (* xp ∪ * xq))
|
|
|
283 gf10 = record { gr = PDN.gr Pp ; pn<gr = gf15 ; x∈PP = subst (λ k → odef L k) (cong (&) (gf131 gp gq)) ( NEG L∋pq ) } where
|
|
|
284 gf16 : gr Pq ≤ gr Pp
|
|
|
285 gf16 = <to≤ c
|
|
|
286 gf15 : (y : Ordinal) → odef (* (& (* xp ∪ * xq))) y → odef (* (find-p L C (gr Pp) (& p0))) y
|
|
|
287 gf15 y gpqy with subst (λ k → odef k y ) *iso gpqy
|
|
|
288 ... | case1 xpy = PDN.pn<gr Pp _ xpy
|
|
|
289 ... | case2 xqy = p-monotonic L p0 C gf16 (PDN.pn<gr Pq y xqy )
|
|
|
290 gf00 : Replace (Replace (PDHOD L p0 C) (λ x → P ＼ x)) (_＼_ P) ≡ PDHOD L p0 C
|
|
|
291 gf00 = ==→o≡ record { eq→ = gf20 ; eq← = gf22 } where
|
|
|
292 gf20 : {x : Ordinal} → odef (Replace (Replace (PDHOD L p0 C) (λ x₁ → P ＼ x₁)) (_＼_ P)) x → PDN L p0 C x
|
|
|
293 gf20 {x} record { z = z₁ ; az = record { z = z ; az = az ; x=ψz = x=ψz₁ } ; x=ψz = x=ψz } =
|
|
|
294 subst (λ k → PDN L p0 C k ) (begin
|
|
|
295 z ≡⟨ sym &iso ⟩
|
|
|
296 & (* z) ≡⟨ cong (&) (sym (L＼Lx=x gf21 )) ⟩
|
|
|
297 & (P ＼ ( P ＼ (* z) )) ≡⟨ cong (λ k → & ( P ＼ k)) (sym *iso) ⟩
|
|
|
298 & (P ＼ (* ( & (P ＼ (* z ))))) ≡⟨ cong (λ k → & (P ＼ (* k))) (sym x=ψz₁) ⟩
|
|
|
299 & (P ＼ (* z₁)) ≡⟨ sym x=ψz ⟩
|
|
|
300 x ∎ ) az where
|
|
|
301 open ≡-Reasoning
|
|
|
302 gf21 : {x : Ordinal } → odef (* z) x → odef P x
|
|
|
303 gf21 {x} lt = L⊆PP ( PDN.x∈PP az) _ lt
|
|
|
304 gf22 : {x : Ordinal} → PDN L p0 C x → odef (Replace (Replace (PDHOD L p0 C) (λ x₁ → P ＼ x₁)) (_＼_ P)) x
|
|
|
305 gf22 {x} pdx = record { z = _ ; az = record { z = _ ; az = pdx ; x=ψz = refl } ; x=ψz = ( begin
|
|
|
306 x ≡⟨ sym &iso ⟩
|
|
|
307 & (* x) ≡⟨ cong (&) (sym (L＼Lx=x gf21 )) ⟩
|
|
|
308 & (P ＼ (P ＼ * x)) ≡⟨ cong (λ k → & ( P ＼ k)) (sym *iso) ⟩
|
|
|
309 & (P ＼ * (& (P ＼ * x))) ∎ ) } where
|
|
|
310 open ≡-Reasoning
|
|
|
311 gf21 : {z : Ordinal } → odef (* x) z → odef P z
|
|
|
312 gf21 {z} lt = L⊆PP ( PDN.x∈PP pdx ) z lt
|
|
|
313 fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D → ¬ (Dense.dense D ∩ (PDHOD L p0 C)) ≡ od∅
|
|
|
314 fdense D MD eq0 = ⊥-elim ( ∅< {Dense.dense D ∩ PDHOD L p0 C} fd01 (≡od∅→=od∅ eq0 )) where
|
|
|
315 open Dense
|
|
1254
|
316 open Expansion
|
|
1248
|
317 fd09 : (i : ℕ ) → odef L (find-p L C i (& p0))
|
|
|
318 fd09 zero = Lp0
|
|
|
319 fd09 (suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) )
|
|
|
320 ... | yes _ = fd09 i
|
|
|
321 ... | no not = fd17 where
|
|
|
322 fd19 = ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
323 fd18 : PGHOD i L C (find-p L C i (& p0)) ∋ fd19
|
|
|
324 fd18 = ODC.x∋minimal O (PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
325 fd17 : odef L ( & (ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))) )
|
|
|
326 fd17 = proj1 fd18
|
|
|
327 an : ℕ
|
|
|
328 an = ctl← C (& (dense D)) MD
|
|
|
329 pn : Ordinal
|
|
|
330 pn = find-p L C an (& p0)
|
|
|
331 pn+1 : Ordinal
|
|
|
332 pn+1 = find-p L C (suc an) (& p0)
|
|
|
333 d=an : dense D ≡ * (ctl→ C an)
|
|
|
334 d=an = begin dense D ≡⟨ sym *iso ⟩
|
|
|
335 * ( & (dense D)) ≡⟨ cong (*) (sym (ctl-iso→ C MD )) ⟩
|
|
|
336 * (ctl→ C an) ∎ where open ≡-Reasoning
|
|
|
337 fd07 : odef (dense D) pn+1
|
|
|
338 fd07 with is-o∅ ( & ( PGHOD an L C (find-p L C an (& p0))) )
|
|
|
339 ... | yes y = ⊥-elim ( ¬x<0 ( _==_.eq→ fd10 fd21 ) ) where
|
|
|
340 L∋pn : L ∋ * (find-p L C an (& p0))
|
|
|
341 L∋pn = subst (λ k → odef L k) (sym &iso) (fd09 an )
|
|
1254
|
342 exp = has-expansion D L∋pn
|
|
|
343 L∋df : L ∋ ( expansion exp )
|
|
|
344 L∋df = (d⊆P D) (dense∋exp exp)
|
|
|
345 pn∋df : (* (ctl→ C an)) ∋ ( expansion exp)
|
|
|
346 pn∋df = subst (λ k → odef k (& ( expansion exp))) d=an (dense∋exp exp )
|
|
|
347 pn⊆df : (y : Ordinal) → odef (* (find-p L C an (& p0))) y → odef (* (& (expansion exp))) y
|
|
|
348 pn⊆df y py = subst (λ k → odef k y ) (sym *iso) (p⊆exp exp py)
|
|
|
349 fd21 : odef (PGHOD an L C (find-p L C an (& p0)) ) (& (expansion exp))
|
|
1248
|
350 fd21 = ⟪ L∋df , ⟪ pn∋df , pn⊆df ⟫ ⟫
|
|
|
351 fd10 : PGHOD an L C (find-p L C an (& p0)) =h= od∅
|
|
|
352 fd10 = ≡o∅→=od∅ y
|
|
|
353 ... | no not = fd27 where
|
|
|
354 fd29 = ODC.minimal O ( PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
355 fd28 : PGHOD an L C (find-p L C an (& p0)) ∋ fd29
|
|
|
356 fd28 = ODC.x∋minimal O (PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq))
|
|
|
357 fd27 : odef (dense D) (& fd29)
|
|
|
358 fd27 = subst (λ k → odef k (& fd29)) (sym d=an) (proj1 (proj2 fd28))
|
|
|
359 fd03 : odef (PDHOD L p0 C) pn+1
|
|
|
360 fd03 = record { gr = suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (suc an)}
|
|
|
361 fd01 : (dense D ∩ PDHOD L p0 C) ∋ (* pn+1)
|
|
|
362 fd01 = ⟪ subst (λ k → odef (dense D) k ) (sym &iso) fd07 , subst (λ k → odef (PDHOD L p0 C) k) (sym &iso) fd03 ⟫
|
|
1250
|
363 gpx→⊆P : {p : Ordinal } → odef GP p → (* p) ⊆ P
|
|
|
364 gpx→⊆P {p} record { z = z ; az = az ; x=ψz = x=ψz } {x} px with subst (λ k → odef k x )
|
|
|
365 (trans (cong (*) x=ψz) *iso) px
|
|
|
366 ... | ⟪ Px , npz ⟫ = Px
|
|
1252
|
367 L∋gpr : {p : HOD } → GPR ∋ p → (L ∋ p) ∧ ( L ∋ (P ＼ p))
|
|
1251
|
368 L∋gpr {p} record { z = zp ; az = record { z = z ; az = az ; x=ψz = x=ψzp } ; x=ψz = x=ψz }
|
|
1252
|
369 = ⟪ subst (λ k → odef L k) fd40 (PDN.x∈PP az) , NEG (subst (λ k → odef L k) fd40 (PDN.x∈PP az)) ⟫ where
|
|
1251
|
370 fd41 : * z ⊆ P
|
|
|
371 fd41 {x} lt = L⊆PP ( PDN.x∈PP az ) _ lt
|
|
|
372 fd40 : z ≡ & p
|
|
|
373 fd40 = begin
|
|
|
374 z ≡⟨ sym &iso ⟩
|
|
|
375 & (* z) ≡⟨ cong (&) (sym (L＼Lx=x fd41 )) ⟩
|
|
|
376 & (P ＼ ( P ＼ * z ) ) ≡⟨ cong (λ k → & (P ＼ k)) (sym *iso) ⟩
|
|
|
377 & (P ＼ * (& ( P ＼ * z ))) ≡⟨ cong (λ k → & (P ＼ * k )) (sym x=ψzp) ⟩
|
|
|
378 & (P ＼ * zp) ≡⟨ sym x=ψz ⟩
|
|
|
379 & p ∎ where open ≡-Reasoning
|
|
1250
|
380 gpr→gp : {p : HOD} → GPR ∋ p → GP ∋ (P ＼ p )
|
|
|
381 gpr→gp {p} record { z = zp ; az = azp ; x=ψz = x=ψzp } = gfp where
|
|
|
382 open ≡-Reasoning
|
|
|
383 gfp : GP ∋ (P ＼ p )
|
|
|
384 gfp = subst (λ k → odef GP k) (begin
|
|
|
385 zp ≡⟨ sym &iso ⟩
|
|
|
386 & (* zp) ≡⟨ cong (&) (sym (L＼Lx=x (gpx→⊆P azp) )) ⟩
|
|
|
387 & (P ＼ (P ＼ (* zp) )) ≡⟨ cong (λ k → & ( P ＼ k)) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym x=ψzp))) ⟩
|
|
|
388 & (P ＼ p) ∎ ) azp
|
|
1254
|
389 gideal1 : {p q : HOD} → GPR ∋ p → q ⊆ p → L ∋ ( P ＼ q) → GPR ∋ q
|
|
|
390 gideal1 {p} {q} record { z = np ; az = record { z = z ; az = pdz ; x=ψz = x=ψznp } ; x=ψz = x=ψz } q⊆p Lpq
|
|
1252
|
391 = record { z = _ ; az = gf30 ; x=ψz = cong (&) fd42 } where
|
|
1250
|
392 gp = record { z = np ; az = record { z = z ; az = pdz ; x=ψz = x=ψznp } ; x=ψz = x=ψz }
|
|
1251
|
393 open ≡-Reasoning
|
|
|
394 fd41 : * z ⊆ P
|
|
|
395 fd41 {x} lt = L⊆PP ( PDN.x∈PP pdz ) _ lt
|
|
|
396 p=*z : p ≡ * z
|
|
|
397 p=*z = trans (sym *iso) ( cong (*) (sym ( begin
|
|
|
398 z ≡⟨ sym &iso ⟩
|
|
|
399 & (* z) ≡⟨ cong (&) (sym (L＼Lx=x fd41 )) ⟩
|
|
|
400 & (P ＼ ( P ＼ * z ) ) ≡⟨ cong (λ k → & (P ＼ k)) (sym *iso) ⟩
|
|
|
401 & (P ＼ * (& ( P ＼ * z ))) ≡⟨ cong (λ k → & (P ＼ * k )) (sym x=ψznp) ⟩
|
|
|
402 & (P ＼ * np) ≡⟨ sym x=ψz ⟩
|
|
|
403 & p ∎ )))
|
|
1250
|
404 q⊆P : q ⊆ P
|
|
1251
|
405 q⊆P {x} lt = L⊆PP ( PDN.x∈PP pdz ) _ (subst (λ k → odef k x) p=*z (q⊆p lt))
|
|
1252
|
406 fd42 : q ≡ P ＼ * (& (P ＼ q))
|
|
|
407 fd42 = trans (sym (L＼Lx=x q⊆P )) (cong (λ k → P ＼ k) (sym *iso) )
|
|
1250
|
408 gf32 : (P ＼ p) ⊆ (P ＼ q)
|
|
|
409 gf32 = proj1 (＼-⊆ {P} {q} {p} q⊆P ) q⊆p
|
|
1248
|
410 gf30 : GP ∋ (P ＼ q )
|
|
1252
|
411 gf30 = f1 Lpq (gpr→gp gp) gf32
|
|
1254
|
412 gideal2 : {p q : HOD} → (GPR ∋ p) ∧ (GPR ∋ q) → Replace GP (_＼_ P) ∋ (p ∪ q)
|
|
|
413 gideal2 {p} {q} ⟪ gp , gq ⟫
|
|
1252
|
414 = record { z = _ ; az = gf31 ; x=ψz = cong (&) gf32 } where
|
|
1250
|
415 open ≡-Reasoning
|
|
1248
|
416 gf31 : GP ∋ ( (P ＼ p ) ∩ (P ＼ q ) )
|
|
1252
|
417 gf31 = f2 (gpr→gp gp) (gpr→gp gq) (CAP (proj2 (L∋gpr gp)) (proj2 (L∋gpr gq)) )
|
|
|
418 gf33 : (p ∪ q) ⊆ P
|
|
|
419 gf33 {x} (case1 px) = L⊆PP (proj1 (L∋gpr gp)) _ (subst (λ k → odef k x) (sym *iso) px )
|
|
|
420 gf33 {x} (case2 qx) = L⊆PP (proj1 (L∋gpr gq)) _ (subst (λ k → odef k x) (sym *iso) qx )
|
|
|
421 gf32 : (p ∪ q) ≡ (P ＼ * (& ((P ＼ p) ∩ (P ＼ q))))
|
|
|
422 gf32 = begin
|
|
|
423 p ∪ q ≡⟨ sym ( L＼Lx=x gf33 ) ⟩
|
|
|
424 P ＼ (P ＼ (p ∪ q)) ≡⟨ cong (λ k → P ＼ k) (sym (gf02 {P} {p}{q} ) ) ⟩
|
|
|
425 P ＼ ((P ＼ p) ∩ (P ＼ q)) ≡⟨ cong (λ k → P ＼ k) (sym *iso) ⟩
|
|
|
426 P ＼ * (& ((P ＼ p) ∩ (P ＼ q))) ∎
|
|
448
|
427
|
|
431
|
428 open GenericFilter
|
|
|
429 open Filter
|
|
|
430
|
|
1245
|
431 record NotCompatible (L p : HOD ) (L∋a : L ∋ p ) : Set (Level.suc (Level.suc n)) where
|
|
431
|
432 field
|
|
1245
|
433 q r : HOD
|
|
|
434 Lq : L ∋ q
|
|
|
435 Lr : L ∋ r
|
|
|
436 p⊆q : p ⊆ q
|
|
|
437 p⊆r : p ⊆ r
|
|
|
438 ¬compat : (s : HOD) → ¬ ( (q ⊆ s) ∧ (r ⊆ s) )
|
|
431
|
439
|
|
1246
|
440 lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
|
|
1245
|
441 → (CAP : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q )) -- L is a Boolean Algebra
|
|
|
442 → (UNI : {p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∪ q ))
|
|
|
443 → (NEG : ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)))
|
|
|
444 → (C : CountableModel )
|
|
1249
|
445 → ctl-M C ∋ L
|
|
1245
|
446 → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp )
|
|
1246
|
447 → ¬ ( ctl-M C ∋ rgen ( P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG C ))
|
|
1254
|
448 lemma232 P L p0 LPP Lp0 CAP UNI NEG C ML NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj1 rgf∩D) (proj2 rgf∩D))
|
|
1245
|
449 ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
|
|
1249
|
450 PG = P-GenericFilter P L p0 LPP Lp0 CAP UNI NEG C
|
|
|
451 GF = genf PG
|
|
|
452 rgf = rgen PG
|
|
1245
|
453 M = ctl-M C
|
|
|
454 D : HOD
|
|
1248
|
455 D = L ＼ rgf
|
|
|
456 M∋DM : M ∋ (D ∩ M )
|
|
1249
|
457 M∋DM = is-model C D ?
|
|
1254
|
458 M∋D : M ∋ D
|
|
|
459 M∋D = ?
|
|
|
460 M∋G : M ∋ rgf
|
|
|
461 M∋G = MF
|
|
1246
|
462 D⊆PP : D ⊆ Power P
|
|
|
463 D⊆PP {x} ⟪ Lx , ngx ⟫ = LPP Lx
|
|
|
464 DD : Dense {L} {P} LPP
|
|
1254
|
465 DD = record { dense = D ; d⊆P = proj1 ; has-expansion = exp } where
|
|
|
466 exp : {p : HOD} → (Lp : L ∋ p) → Expansion L D Lp
|
|
|
467 exp {p} Lp = exp1 where
|
|
|
468 q : HOD
|
|
|
469 q = NotCompatible.q (NC Lp)
|
|
|
470 r : HOD
|
|
|
471 r = NotCompatible.r (NC Lp)
|
|
|
472 exp1 : Expansion L D Lp
|
|
|
473 exp1 with ODC.p∨¬p O (rgf ∋ q)
|
|
|
474 ... | case2 ngq = record { expansion = q ; dense∋exp = ? ; p⊆exp = ? }
|
|
|
475 ... | case1 gq with ODC.p∨¬p O (rgf ∋ r)
|
|
|
476 ... | case2 ngr = record { expansion = q ; dense∋exp = ? ; p⊆exp = ? }
|
|
|
477 ... | case1 gr = ⊥-elim ( ll02 ⟪ ? , ? ⟫ ) where
|
|
|
478 ll02 : ¬ ( (q ⊆ p) ∧ (r ⊆ p) )
|
|
|
479 ll02 = NotCompatible.¬compat (NC Lp) p
|
|
|
480 ll03 : rgf ∋ p → rgf ∋ q → rgf ∋ (p ∪ q)
|
|
|
481 ll03 rp rq = gideal2 PG ⟪ rp , rq ⟫
|
|
|
482 ll04 : rgf ∋ p → q ⊆ p → rgf ∋ q
|
|
|
483 ll04 rp q⊆p = gideal1 PG rp q⊆p ?
|
|
|
484 ¬rgf∩D=0 : ¬ ( (D ∩ rgf ) =h= od∅ )
|
|
|
485 ¬rgf∩D=0 eq = generic PG DD M∋D (==→o≡ eq)
|
|
431
|
486
|
|
|
487 --
|
|
1174
|
488 -- P-Generic Filter defines a countable model D ⊂ C from P
|
|
|
489 --
|
|
|
490
|
|
|
491 --
|
|
|
492 -- in D, we have V ≠ L
|
|
|
493 --
|
|
|
494
|
|
|
495 --
|
|
431
|
496 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
|
|
|
497 --
|
|
436
|
498
|
|
1242
|
499 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
|
500 field
|
|
|
501 valx : HOD
|
|
436
|
502
|
|
437
|
503 record valS (ox oy oG : Ordinal) : Set n where
|
|
436
|
504 field
|
|
437
|
505 op : Ordinal
|
|
1244
|
506 p∈G : odef (* oG) op
|
|
437
|
507 is-val : odef (* ox) ( & < * oy , * op > )
|
|
436
|
508
|
|
459
|
509 val : (x : HOD) {P L : HOD } {LP : L ⊆ Power P}
|
|
1096
|
510 → (G : GenericFilter {L} {P} LP {!!} )
|
|
436
|
511 → HOD
|
|
437
|
512 val x G = TransFinite {λ x → HOD } ind (& x) where
|
|
|
513 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → HOD) → HOD
|
|
439
|
514 ind x valy = record { od = record { def = λ y → valS x y (& (filter (genf G))) } ; odmax = {!!} ; <odmax = {!!} }
|
|
437
|
515
|
