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

comparison src/generic-filter.agda @ 1174:375615f9d60f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Func and Funcs
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 Feb 2023 11:51:22 +0900
parents d122d0c1b094
children 42000f20fdbe
comparison
equal deleted inserted replaced
1173:4b2f49a5a1d5 1174:375615f9d60f
59 ctl-M : HOD 59 ctl-M : HOD
60 ctl→ : Nat → Ordinal 60 ctl→ : Nat → Ordinal
61 ctl<M : (x : Nat) → odef (ctl-M) (ctl→ x) 61 ctl<M : (x : Nat) → odef (ctl-M) (ctl→ x)
62 ctl← : (x : Ordinal )→ odef (ctl-M ) x → Nat 62 ctl← : (x : Ordinal )→ odef (ctl-M ) x → Nat
63 ctl-iso→ : { x : Ordinal } → (lt : odef (ctl-M) x ) → ctl→ (ctl← x lt ) ≡ x 63 ctl-iso→ : { x : Ordinal } → (lt : odef (ctl-M) x ) → ctl→ (ctl← x lt ) ≡ x
64 ctl-iso← : { x : Nat } → ctl← (ctl→ x ) (ctl<M x) ≡ x 64 -- we have no otherway round
65 -- ctl-iso← : { x : Nat } → ctl← (ctl→ x ) (ctl<M x) ≡ x
65 -- 66 --
66 -- almmost universe 67 -- almmost universe
67 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x 68 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
68 -- 69 --
69 70
239 lemma232 P L p C LP Lp0 NA MG = {!!} where 240 lemma232 P L p C LP Lp0 NA MG = {!!} where
240 D : HOD -- P - G 241 D : HOD -- P - G
241 D = ? 242 D = ?
242 243
243 -- 244 --
245 -- P-Generic Filter defines a countable model D ⊂ C from P
246 --
247
248 --
249 -- in D, we have V ≠ L
250 --
251
252 --
244 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > } 253 -- val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
245 -- 254 --
246 255
247 record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (C : CountableModel ) (G : GenericFilter {L} {P} LP (ctl-M C) ) : Set (suc n) where 256 record valR (x : HOD) {P L : HOD} {LP : L ⊆ Power P} (C : CountableModel ) (G : GenericFilter {L} {P} LP (ctl-M C) ) : Set (suc n) where
248 field 257 field