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

comparison generic-filter.agda @ 413:b00d58b3dc57

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generic filter on going
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 30 Jul 2020 08:15:56 +0900
parents 38eded55c72d
children 44a484f17f26
comparison
equal deleted inserted replaced
412:38eded55c72d 413:b00d58b3dc57
205 px∈ω : odef (Power P) x 205 px∈ω : odef (Power P) x
206 206
207 open PDN 207 open PDN
208 208
209 --- 209 ---
210 -- G as an HOD 210 -- G as a HOD
211 -- 211 --
212 PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD 212 PDHOD : (C : CountableOrdinal) → (P : HOD ) → HOD
213 PDHOD C P = record { od = record { def = λ x → PDN C P x } 213 PDHOD C P = record { od = record { def = λ x → PDN C P x }
214 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.px∈ω lt) } where 214 ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.px∈ω lt) } where
215 215
216 open PDN
217
218 ----
219 -- Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set )
216 -- 220 --
217 -- p 0 ≡ ∅ 221 -- p 0 ≡ ∅
218 -- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q 222 -- p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q (axiom of choice)
219 --- else p n 223 --- else p n
220 224
221 open PDN
222
223 ----
224 -- Generic Filter on Power P for HOD's Ordinal
225 --
226 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P 225 P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
227 P-GenericFilter C P = record { 226 P-GenericFilter C P = record {
228 genf = record { filter = PDHOD C P ; f⊆PL = f⊆PL ; filter1 = {!!} ; filter2 = {!!} } 227 genf = record { filter = PDHOD C P ; f⊆PL = f⊆PL ; filter1 = {!!} ; filter2 = {!!} }
229 ; generic = λ D → {!!} 228 ; generic = λ D → {!!}
230 } where 229 } where
231 find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal) → odef (ord→od (find-p C P i x)) y → odef P y 230 P∅ : {P : HOD} → odef (Power P) o∅
232 find-p-⊆P C P Zero x y Py = {!!} 231 P∅ {P} = subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅ o∅≡od∅) where
233 find-p-⊆P C P (Suc i) x y Py = {!!} -- find-p-⊆P C P i x {!!} 232 lemma : (x : Ordinal ) → ord→od x ≡ od∅ → odef (Power P) (od→ord od∅)
233 lemma x eq = power← P od∅ (λ {x} lt → ⊥-elim (¬x<0 lt ))
234 x<y→∋ : {x y : Ordinal} → odef (ord→od x) y → ord→od x ∋ ord→od y
235 x<y→∋ {x} {y} lt = subst (λ k → odef (ord→od x) k ) (sym diso) lt
236 find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal) → odef (Power P) x → odef (ord→od (find-p C P i x)) y → odef P y
237 find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) diso
238 ( incl (ODC.power→⊆ O P (ord→od x) (d→∋ (Power P) Px)) (x<y→∋ Py))
239 find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p C P i x) y {!!} {!!}
234 f⊆PL : PDHOD C P ⊆ Power P 240 f⊆PL : PDHOD C P ⊆ Power P
235 f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x → 241 f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
236 find-p-⊆P C P (gr lt) o∅ (od→ord y) (pn<gr lt (od→ord y) (subst (λ k → odef k (od→ord y)) (sym oiso) y<x))) } 242 find-p-⊆P C P (gr lt) o∅ (od→ord y) P∅ (pn<gr lt (od→ord y) (subst (λ k → odef k (od→ord y)) (sym oiso) y<x))) }
237 243
238 244
239 open GenericFilter 245 open GenericFilter
240 open Filter 246 open Filter
241 247