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

comparison HOD.agda @ 121:453ef0d4ee8a

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 Thu, 27 Jun 2019 19:26:45 +0900
parents ac214eab1c3c
children 4d2434513228
comparison
equal deleted inserted replaced
120:ac214eab1c3c 121:453ef0d4ee8a
219 csuc x = ord→od ( osuc ( od→ord x )) 219 csuc x = ord→od ( osuc ( od→ord x ))
220 220
221 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) 221 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
222 222
223 ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n} 223 ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n}
224 ZFSubset A x = record { def = λ y → def A y ∧ def x y ; otrans = {!!} } 224 ZFSubset A x = record { def = λ y → def A y ∧ def x y ; otrans = lemma } where
225 lemma : {z : Ordinal} → def A z ∧ def x z → {y : Ordinal} → y o< z → def A y ∧ def x y
226 lemma {z} d {y} y<z = record { proj1 = otrans A (proj1 d) y<z ; proj2 = otrans x (proj2 d) y<z }
225 227
226 Def : {n : Level} → (A : HOD {suc n}) → HOD {suc n} 228 Def : {n : Level} → (A : HOD {suc n}) → HOD {suc n}
227 Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) 229 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
228 230
229 -- Constructible Set on α 231 -- Constructible Set on α
230 L : {n : Level} → (α : Ordinal {suc n}) → HOD {suc n} 232 L : {n : Level} → (α : Ordinal {suc n}) → HOD {suc n}
231 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅ 233 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅
232 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) 234 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) )
233 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) 235 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
234 record { def = λ y → osuc y o< (od→ord (L {n} (record { lv = lx ; ord = Φ lx }) )) ; otrans = {!!} } 236 cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx }))))
235 237
236 omega : { n : Level } → Ordinal {n} 238 omega : { n : Level } → Ordinal {n}
237 omega = record { lv = Suc Zero ; ord = Φ 1 } 239 omega = record { lv = Suc Zero ; ord = Φ 1 }
238 240
239 HOD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 241 HOD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
316 -- In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity 318 -- In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity
317 -- 319 --
318 power→ : (A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x 320 power→ : (A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
319 power→ A t P∋t {x} t∋x = proj1 lemma-s where 321 power→ A t P∋t {x} t∋x = proj1 lemma-s where
320 minsup : HOD 322 minsup : HOD
321 minsup = ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 323 minsup = ZFSubset A ( Ord ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))
322 lemma-t : csuc minsup ∋ t 324 lemma-t : csuc minsup ∋ t
323 lemma-t = {!!} -- o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl ) 325 lemma-t = {!!} -- o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl )
324 lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) ∋ x 326 lemma-s : ZFSubset A ( Ord ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) ∋ x
325 lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso ) 327 lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso )
326 lemma-s | case1 eq = def-subst {!!} oiso refl 328 lemma-s | case1 eq = {!!}
327 lemma-s | case2 lt = transitive {n} {minsup} {t} {x} (def-subst {!!} oiso refl ) t∋x 329 lemma-s | case2 lt = transitive {n} {minsup} {t} {x} {!!} t∋x
328 -- 330 --
329 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t 331 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
330 -- Power A is a sup of ZFSubset A t, so Power A ∋ t 332 -- Power A is a sup of ZFSubset A t, so Power A ∋ t
331 -- 333 --
332 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t 334 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t