Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/generic-filter.agda @ 448:81691a6b352b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Mar 2022 19:03:33 +0900
parents 364d738f871d
children be685f338fdc
comparison
equal deleted inserted replaced
447:364d738f871d 448:81691a6b352b
147 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c ) 147 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> n≤m c )
148 148
149 P-GenericFilter : (P p0 : HOD ) → Power P ∋ p0 → (C : CountableModel P) → GenericFilter P 149 P-GenericFilter : (P p0 : HOD ) → Power P ∋ p0 → (C : CountableModel P) → GenericFilter P
150 P-GenericFilter P p0 Pp0 C = record { 150 P-GenericFilter P p0 Pp0 C = record {
151 genf = record { filter = PDHOD P p0 C ; f⊆PL = f⊆PL ; filter1 = f1 ; filter2 = f2 } 151 genf = record { filter = PDHOD P p0 C ; f⊆PL = f⊆PL ; filter1 = f1 ; filter2 = f2 }
152 ; generic = λ D → {!!} 152 ; generic = fdense
153 } where 153 } where
154 PGHOD∈PL : (i : Nat) → (x : Ordinal) → PGHOD i P C x ⊆ Power P 154 PGHOD∈PL : (i : Nat) → (x : Ordinal) → PGHOD i P C x ⊆ Power P
155 PGHOD∈PL i x = record { incl = λ {x} p → proj1 p } 155 PGHOD∈PL i x = record { incl = λ {x} p → proj1 p }
156 f⊆PL : PDHOD P p0 C ⊆ Power P 156 f⊆PL : PDHOD P p0 C ⊆ Power P
157 f⊆PL = record { incl = λ {x} lt → x∈PP lt } 157 f⊆PL = record { incl = λ {x} lt → x∈PP lt }
162 -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y 162 -- odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (& q)) y
163 f2 : {p q : HOD} → PDHOD P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q) 163 f2 : {p q : HOD} → PDHOD P p0 C ∋ p → PDHOD P p0 C ∋ q → PDHOD P p0 C ∋ (p ∩ q)
164 f2 {p} {q} PD∋p PD∋q with <-cmp (gr PD∋p) (gr PD∋q) 164 f2 {p} {q} PD∋p PD∋q with <-cmp (gr PD∋p) (gr PD∋q)
165 ... | tri< a ¬b ¬c = record { gr = gr PD∋p ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt); x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where 165 ... | tri< a ¬b ¬c = record { gr = gr PD∋p ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt); x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where
166 f3 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y 166 f3 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
167 f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y ?) ⟫ 167 f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y (f5 lt)) ⟫ where
168 f5 : odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (* (find-p P C (gr PD∋q) (& p0))) y
169 f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋p} {gr PD∋q} (<to≤ a))
170 (subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) (sym &iso) lt) )
171 -- subst (λ k → odef k y) *iso (pn<gr PD∋q y (subst (λ k → odef _ k ) &iso (incl (p-monotonic _ _ C a ) (subst (λ k → odef _ k) &iso lt) ))) ⟫
168 ... | tri≈ ¬a refl ¬c = record { gr = gr PD∋p ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f4 y lt); x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where 172 ... | tri≈ ¬a refl ¬c = record { gr = gr PD∋p ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f4 y lt); x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where
169 f4 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y 173 f4 : (y : Ordinal) → odef (* (find-p P C (gr PD∋p) (& p0))) y → odef (p ∩ q) y
170 f4 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ 174 f4 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y lt) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫
171 ... | tri> ¬a ¬b c = record { gr = gr PD∋q ; pn<gr = {!!} ; x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } 175 ... | tri> ¬a ¬b c = record { gr = gr PD∋q ; pn<gr = λ y lt → subst (λ k → odef k y ) (sym *iso) (f3 y lt) ; x∈PP = ODC.power-∩ O (x∈PP PD∋p) (x∈PP PD∋q) } where
176 f3 : (y : Ordinal) → odef (* (find-p P C (gr PD∋q) (& p0))) y → odef (p ∩ q) y
177 f3 y lt = ⟪ subst (λ k → odef k y) *iso (pn<gr PD∋p y (f5 lt)) , subst (λ k → odef k y) *iso (pn<gr PD∋q y lt) ⟫ where
178 f5 : odef (* (find-p P C (gr PD∋q) (& p0))) y → odef (* (find-p P C (gr PD∋p) (& p0))) y
179 f5 lt = subst (λ k → odef (* (find-p P C (gr PD∋p) (& p0))) k ) &iso ( incl (p-monotonic P p0 C {gr PD∋q} {gr PD∋p} (<to≤ c))
180 (subst (λ k → odef (* (find-p P C (gr PD∋q) (& p0))) k ) (sym &iso) lt) )
181 fdense : (D : Dense P ) → ¬ (filter.Dense.dense D ∩ PDHOD P p0 C) ≡ od∅
182 fdense D eq0 = ⊥-elim ( ∅< {Dense.dense D ∩ PDHOD P p0 C} fd01 (≡od∅→=od∅ eq0 )) where
183 open Dense
184 fd : HOD
185 fd = dense-f D p0
186 PP∋D : dense D ⊆ Power P
187 PP∋D = d⊆P D
188 fd02 : dense D ∋ dense-f D p0
189 fd02 = dense-d D (ODC.power→⊆ O _ _ Pp0 )
190 fd03 : PDHOD P p0 C ∋ dense-f D p0
191 fd03 = f1 {p0} {dense-f D p0} {!!} {!!} ( dense-p D {!!} )
192 fd01 : (dense D ∩ PDHOD P p0 C) ∋ fd
193 fd01 = ⟪ fd02 , fd03 ⟫
194
172 195
173 196
174 197
175 open GenericFilter 198 open GenericFilter
176 open Filter 199 open Filter