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

comparison src/Topology.agda @ 1194:6174001ba1c0

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 Tue, 28 Feb 2023 15:01:17 +0900
parents e110b56d8cbe
children 68239d102d15
comparison
equal deleted inserted replaced
1190:e110b56d8cbe 1194:6174001ba1c0
387 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L) 387 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L)
388 (fip70 o∅ (finCoverBase xo xcp)) where 388 (fip70 o∅ (finCoverBase xo xcp)) where
389 fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x) 389 fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x)
390 fip70 x (gi rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } 390 fip70 x (gi rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt }
391 fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers 391 fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers
392 (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} ? ? ) where 392 (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where
393 fip71 : {a b c : HOD} → a covers c → (a ∪ b) covers c
394 fip71 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case1 (P∋cover cov lt)
395 ; isCover = isCover cov }
396 fip72 : {a b c : HOD} → a covers c → (b ∪ a) covers c
397 fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt)
398 ; isCover = isCover cov }
393 fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪ (L ＼ b)) 399 fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪ (L ＼ b))
394 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x) 400 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x)
395 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫ 401 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫
396 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫ 402 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫
397 fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) ) 403 fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) )
422 OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top 428 OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top
423 OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox 429 OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox
424 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01)) where 430 ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01)) where
425 comp01 : odef (* X) (& (* z)) 431 comp01 : odef (* X) (& (* z))
426 comp01 = subst (λ k → odef (* X) k) (sym &iso) az 432 comp01 = subst (λ k → odef (* X) k) (sym &iso) az
427
428 -- if all finite intersection of X contains something, 433 -- if all finite intersection of X contains something,
429 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) 434 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
430 -- it means there is a limit 435 -- it means there is a limit
431 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) 436 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x)
432 → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ ) 437 → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ )
434 fp07 : HOD -- we have an element of X 439 fp07 : HOD -- we have an element of X
435 fp07 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) 440 fp07 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
436 fp08 : odef (* X) (& fp07) 441 fp08 : odef (* X) (& fp07)
437 fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) 442 fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
438 no-cover : ¬ ( (* (OX CX)) covers L ) 443 no-cover : ¬ ( (* (OX CX)) covers L )
439 no-cover cov = ⊥-elim ( ? ) where 444 no-cover cov = ⊥-elim ( SB.¬i⊆Ut (fp02 fp01 (Compact.isFinite compact (OOX CX) cov) ) fp12 ) where
440 fp01 : Ordinal 445 fp01 : Ordinal
441 fp01 = Compact.finCover compact (OOX CX) cov 446 fp01 = Compact.finCover compact (OOX CX) cov
442 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L ＼ * t ) ) 447 record SB (t : Ordinal) : Set n where
443 fp02 t fin-e = gi ? 448 field
444 fp02 t (fin-i tx ) = gi fp03 where 449 i : Ordinal
445 fp03 : odef (* X) (& (L ＼ * t)) 450 ¬i⊆Ut : ¬ ( (L ＼ * i) ⊆ Union (* t))
446 fp03 = ? 451 sb : Subbase (* X) (& (L ＼ * i))
447 fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (fp02 tx x) (fp02 ty y ) ) where 452 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t
448 fp04 : & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) 453 fp02 t fin-e = record { i = & ( L ＼ fp07) ; ¬i⊆Ut = fp20 ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) } where
449 fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where 454 fp22 : fp07 ⊆ L
455 fp22 {x} lt = cs⊆L top (CX fp08) lt
456 fp21 : & fp07 ≡ & (L ＼ * (& (L ＼ fp07)))
457 fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼ k) (sym *iso)))
458 fp20 : ¬ (L ＼ * (& (L ＼ fp07))) ⊆ Union (* o∅)
459 fp20 lt = ?
460 fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; ¬i⊆Ut = fp23 } where
461 fp23 : ¬ (L ＼ * x) ⊆ Union (* (& (* x , * x)))
462 fp23 = ?
463 fp03 : odef (* X) (& (L ＼ * x))
464 fp03 with subst (λ k → odef k x ) *iso tx
465 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
466 fip34 : * z1 ⊆ L
467 fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1
468 fip33 : z1 ≡ & (L ＼ * x)
469 fip33 = begin
470 z1 ≡⟨ sym &iso ⟩
471 & (* z1) ≡⟨ cong (&) (sym (L＼Lx=x fip34 )) ⟩
472 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
473 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
474 & (L ＼ * x ) ∎ where open ≡-Reasoning
475 fp02 t (fin-∪ {tx} {ty} x y ) = record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 ; ¬i⊆Ut = ? } where
476 fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
477 fp04 {tx} {ty} = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where
450 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x 478 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x
451 fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt 479 fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt
452 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫ where 480 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫ where
453 fp06 : ¬ odef (* tx ∪ * ty) x 481 fp06 : ¬ odef (* tx ∪ * ty) x
454 fp06 (case1 tx) = ¬tx tx 482 fp06 (case1 tx) = ¬tx tx
455 fp06 (case2 ty) = ¬ty ty 483 fp06 (case2 ty) = ¬ty ty
456 fp09 : {x : Ordinal} → odef (L ＼ * (& (* tx ∪ * ty))) x → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x 484 fp09 : {x : Ordinal} → odef (L ＼ * (& (* tx ∪ * ty))) x → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x
457 fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt 485 fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt
458 ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso) 486 ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso)
459 ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫ 487 ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫
460 488 fp11 : Subbase (* X) (& (L ＼ * (& ((* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y)))))))
489 fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx x)) (SB.sb (fp02 ty y )) )
490 fp12 : (L ＼ * (SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov)))) ⊆ Union (* fp01)
491 fp12 {x} ⟪ Lx , not ⟫ = ⊥-elim ( fp14 (λ {y} lt → record { owner = cover fcov (fp16 lt)
492 ; ao = P∋cover fcov (fp16 lt)
493 ; ox = isCover fcov (fp16 lt) } )) where
494 fcov = Compact.isCover compact (OOX CX) cov
495 fp13 : Ordinal
496 fp13 = SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov))
497 fp16 : {y : Ordinal} → odef (L ＼ * fp13) y → odef L y
498 fp16 {y} ⟪ Ly , _ ⟫ = Ly
499 fp15 : ¬ ( odef (* fp13) x)
500 fp15 = not
501 fp14 : ¬ ( (L ＼ * fp13 ) ⊆ Union (* fp01 ))
502 fp14 = SB.¬i⊆Ut (fp02 fp01 (Compact.isFinite compact (OOX CX) cov))
461 record NC : Set n where -- x is not covered 503 record NC : Set n where -- x is not covered
462 field 504 field
463 x : Ordinal 505 x : Ordinal
464 yx : {y : Ordinal} (Xy : odef (* X) y) → odef (* y) x 506 yx : {y : Ordinal} (Xy : odef (* X) y) → odef (* y) x
465 not-covered : NC 507 not-covered : NC