Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 300:e70980bd80c7
-- the set of finite partial functions from ω to 2
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 23 Jun 2020 15:12:43 +0900 |
parents | ef93c56ad311 |
children | b012a915bbb5 |
comparison
equal
deleted
inserted
replaced
296:42f89e5efb00 | 300:e70980bd80c7 |
---|---|
206 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) | 206 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) |
207 | 207 |
208 ZFSubset : (A x : OD ) → OD | 208 ZFSubset : (A x : OD ) → OD |
209 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set | 209 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set |
210 | 210 |
211 Def : (A : OD ) → OD | 211 OPwr : (A : OD ) → OD |
212 Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) ) | 212 OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) ) |
213 | 213 |
214 -- _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n | 214 -- _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n |
215 -- _⊆_ A B {x} = A ∋ x → B ∋ x | 215 -- _⊆_ A B {x} = A ∋ x → B ∋ x |
216 | 216 |
217 record _⊆_ ( A B : OD ) : Set (suc n) where | 217 record _⊆_ ( A B : OD ) : Set (suc n) where |
266 Union : OD → OD | 266 Union : OD → OD |
267 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } | 267 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } |
268 _∈_ : ( A B : ZFSet ) → Set n | 268 _∈_ : ( A B : ZFSet ) → Set n |
269 A ∈ B = B ∋ A | 269 A ∈ B = B ∋ A |
270 Power : OD → OD | 270 Power : OD → OD |
271 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) | 271 Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) |
272 -- {_} : ZFSet → ZFSet | 272 -- {_} : ZFSet → ZFSet |
273 -- { x } = ( x , x ) -- it works but we don't use | 273 -- { x } = ( x , x ) -- it works but we don't use |
274 | 274 |
275 data infinite-d : ( x : Ordinal ) → Set n where | 275 data infinite-d : ( x : Ordinal ) → Set n where |
276 iφ : infinite-d o∅ | 276 iφ : infinite-d o∅ |
367 proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; | 367 proj1 = def-subst {_} {_} {b} {x} (inc (def-subst {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; |
368 eq← = λ {x} x<a∩b → proj2 x<a∩b } | 368 eq← = λ {x} x<a∩b → proj2 x<a∩b } |
369 -- | 369 -- |
370 -- Transitive Set case | 370 -- Transitive Set case |
371 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t == t | 371 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t == t |
372 -- Def (Ord a) is a sup of ZFSubset (Ord a) t, so Def (Ord a) ∋ t | 372 -- OPwr (Ord a) is a sup of ZFSubset (Ord a) t, so OPwr (Ord a) ∋ t |
373 -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) | 373 -- OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) |
374 -- | 374 -- |
375 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t | 375 ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t |
376 ord-power← a t t→A = def-subst {_} {_} {Def (Ord a)} {od→ord t} | 376 ord-power← a t t→A = def-subst {_} {_} {OPwr (Ord a)} {od→ord t} |
377 lemma refl (lemma1 lemma-eq )where | 377 lemma refl (lemma1 lemma-eq )where |
378 lemma-eq : ZFSubset (Ord a) t == t | 378 lemma-eq : ZFSubset (Ord a) t == t |
379 eq→ lemma-eq {z} w = proj2 w | 379 eq→ lemma-eq {z} w = proj2 w |
380 eq← lemma-eq {z} w = record { proj2 = w ; | 380 eq← lemma-eq {z} w = record { proj2 = w ; |
381 proj1 = def-subst {_} {_} {(Ord a)} {z} | 381 proj1 = def-subst {_} {_} {(Ord a)} {z} |
385 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) | 385 lemma1 {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq )) |
386 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) x)) | 386 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) x)) |
387 lemma = sup-o< | 387 lemma = sup-o< |
388 | 388 |
389 -- | 389 -- |
390 -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first | 390 -- Every set in OD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first |
391 -- then replace of all elements of the Power set by A ∩ y | 391 -- then replace of all elements of the Power set by A ∩ y |
392 -- | 392 -- |
393 -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) | 393 -- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y ) |
394 | 394 |
395 -- we have oly double negation form because of the replacement axiom | 395 -- we have oly double negation form because of the replacement axiom |
396 -- | 396 -- |
397 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) | 397 power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) |
398 power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where | 398 power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where |
399 a = od→ord A | 399 a = od→ord A |
400 lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y))) | 400 lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y))) |
401 lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t | 401 lemma2 = replacement→ (OPwr (Ord (od→ord A))) t P∋t |
402 lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x) | 402 lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x) |
403 lemma3 y eq not = not (proj1 (eq→ eq t∋x)) | 403 lemma3 y eq not = not (proj1 (eq→ eq t∋x)) |
404 lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y))) | 404 lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y))) |
405 lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 )) | 405 lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 )) |
406 lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → ¬ ¬ (def A (od→ord x)) | 406 lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → ¬ ¬ (def A (od→ord x)) |
409 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t | 409 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t |
410 power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where | 410 power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where |
411 a = od→ord A | 411 a = od→ord A |
412 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x | 412 lemma0 : {x : OD} → t ∋ x → Ord a ∋ x |
413 lemma0 {x} t∋x = c<→o< (t→A t∋x) | 413 lemma0 {x} t∋x = c<→o< (t→A t∋x) |
414 lemma3 : Def (Ord a) ∋ t | 414 lemma3 : OPwr (Ord a) ∋ t |
415 lemma3 = ord-power← a t lemma0 | 415 lemma3 = ord-power← a t lemma0 |
416 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t | 416 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t |
417 lemma4 = let open ≡-Reasoning in begin | 417 lemma4 = let open ≡-Reasoning in begin |
418 A ∩ ord→od (od→ord t) | 418 A ∩ ord→od (od→ord t) |
419 ≡⟨ cong (λ k → A ∩ k) oiso ⟩ | 419 ≡⟨ cong (λ k → A ∩ k) oiso ⟩ |
422 t | 422 t |
423 ∎ | 423 ∎ |
424 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x)) | 424 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x)) |
425 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x))) | 425 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x))) |
426 lemma4 (sup-o< {λ x → od→ord (A ∩ x)} ) | 426 lemma4 (sup-o< {λ x → od→ord (A ∩ x)} ) |
427 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) | 427 lemma2 : def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) |
428 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where | 428 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where |
429 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) | 429 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) |
430 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) | 430 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) |
431 | 431 |
432 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) | 432 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) |