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

comparison src/Topology.agda @ 1197:0a88fcd5d1c9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... almost
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 01 Mar 2023 00:37:34 +0900
parents e7c3bd9e7c3e
children 6e0cc71097e0
comparison
equal deleted inserted replaced
1196:e7c3bd9e7c3e 1197:0a88fcd5d1c9
418 open _==_ 418 open _==_
419 419
420 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top 420 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top
421 Compact→FIP {L} top compact with trio< (& L) o∅ 421 Compact→FIP {L} top compact with trio< (& L) o∅
422 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 422 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
423 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? } 423 ... | tri≈ ¬a b ¬c = record { limit = λ {X} CX fip → o∅ ; is-limit = λ {X} CX fip xx → ⊥-elim (fip000 CX xx) } where
424 fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ¬ odef (* X) x
425 fip000 {X} {x} CX xx = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) b)) o∅≡od∅ ) (sym &iso)
426 ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx)) ? ))
427 -- (subst (λ k → odef (CS top) k) (sym &iso) ( CX xx ) ) ))
424 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where 428 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
425 -- set of coset of X 429 -- set of coset of X
426 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal 430 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
427 OX {X} ox = & ( Replace (* X) (λ z → L ＼ z )) 431 OX {X} ox = & ( Replace (* X) (λ z → L ＼ z ))
428 OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top 432 OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top
448 field 452 field
449 i : Ordinal 453 i : Ordinal
450 sb : Subbase (* X) (& (L ＼ * i)) 454 sb : Subbase (* X) (& (L ＼ * i))
451 not-t : (L ＼ * i) ⊆ (L ＼ Union ( * t ) ) 455 not-t : (L ＼ * i) ⊆ (L ＼ Union ( * t ) )
452 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t 456 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t
453 fp02 t fin-e = record { i = & ( L ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) ; not-t = ? } where 457 fp02 t fin-e = record { i = & ( L ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) ; not-t = fp23 } where
454 fp22 : fp07 ⊆ L 458 fp22 : fp07 ⊆ L
455 fp22 {x} lt = cs⊆L top (CX fp08) lt 459 fp22 {x} lt = cs⊆L top (CX fp08) lt
456 fp21 : & fp07 ≡ & (L ＼ * (& (L ＼ fp07))) 460 fp21 : & fp07 ≡ & (L ＼ * (& (L ＼ fp07)))
457 fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼ k) (sym *iso))) 461 fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼ k) (sym *iso)))
458 fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; not-t = ? } where 462 fp23 : (L ＼ * (& (L ＼ fp07))) ⊆ (L ＼ Union (* o∅))
463 fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) (Own.ao lt )))) ⟫
464 fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; not-t = fp24 } where
465 fp24 : (L ＼ * x) ⊆ (L ＼ Union (* (& (* x , * x))))
466 fp24 {y} ⟪ Lx , not ⟫ = ⟪ Lx , subst (λ k → ¬ odef (Union k) y) (sym *iso) fp25 ⟫ where
467 fp25 : ¬ odef (Union (* x , * x)) y
468 fp25 record { owner = .(& (* x)) ; ao = (case1 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox )
469 fp25 record { owner = .(& (* x)) ; ao = (case2 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox )
459 fp03 : odef (* X) (& (L ＼ * x)) 470 fp03 : odef (* X) (& (L ＼ * x))
460 fp03 with subst (λ k → odef k x ) *iso tx 471 fp03 with subst (λ k → odef k x ) *iso tx
461 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where 472 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
462 fip34 : * z1 ⊆ L 473 fip34 : * z1 ⊆ L
463 fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1 474 fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1
466 z1 ≡⟨ sym &iso ⟩ 477 z1 ≡⟨ sym &iso ⟩
467 & (* z1) ≡⟨ cong (&) (sym (L＼Lx=x fip34 )) ⟩ 478 & (* z1) ≡⟨ cong (&) (sym (L＼Lx=x fip34 )) ⟩
468 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩ 479 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
469 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩ 480 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
470 & (L ＼ * x ) ∎ where open ≡-Reasoning 481 & (L ＼ * x ) ∎ where open ≡-Reasoning
471 fp02 t (fin-∪ {tx} {ty} x y ) = record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 ; not-t = ? } where 482 fp02 t (fin-∪ {tx} {ty} x y ) = record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 ; not-t = fp35 } where
483 fp35 : (L ＼ * (& (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))))) ⊆ (L ＼ Union (* (& (* tx ∪ * ty))))
484 fp35 = subst₂ (λ j k → (L ＼ j ) ⊆ (L ＼ Union k)) (sym *iso) (sym *iso) fp36 where
485 fp40 : {z tz : Ordinal } → Finite-∪ (* (OX CX)) tz → odef (Union (* tz )) z → odef L z
486 fp40 {z} {.(Ordinals.o∅ O)} fin-e record { owner = owner ; ao = ao ; ox = ox } = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) ao ))
487 fp40 {z} {.(& (* _ , * _))} (fin-i {w} x) uz = fp41 x (subst (λ k → odef (Union k) z) *iso uz) where
488 fp41 : (x : odef (* (OX CX)) w) → (uz : odef (Union (* w , * w)) z ) → odef L z
489 fp41 x record { owner = .(& (* w)) ; ao = (case1 refl) ; ox = ox } =
490 os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) *iso ox )
491 fp41 x record { owner = .(& (* w)) ; ao = (case2 refl) ; ox = ox } =
492 os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) *iso ox )
493 fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz with subst (λ k → odef (Union k) z ) *iso uz
494 ... | record { owner = o ; ao = case1 x1o ; ox = oz } = fp40 ftx record { owner = o ; ao = x1o ; ox = oz }
495 ... | record { owner = o ; ao = case2 y1o ; ox = oz } = fp40 fty record { owner = o ; ao = y1o ; ox = oz }
496 fp36 : (L ＼ (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* tx ∪ * ty))
497 fp36 {z} ⟪ Lz , not ⟫ = ⟪ Lz , fp37 ⟫ where
498 fp37 : ¬ odef (Union (* tx ∪ * ty)) z
499 fp37 record { owner = owner ; ao = (case1 ax) ; ox = ox } = not (case1 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where
500 fp38 : (L ＼ (* (SB.i (fp02 tx x)))) ⊆ (L ＼ Union (* tx))
501 fp38 = SB.not-t (fp02 tx x)
502 fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx x)))
503 fp39 {w} txw with ∨L＼X {L} {* (SB.i (fp02 tx x))} (fp40 x txw)
504 ... | case1 sb = sb
505 ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw )
506 fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where
507 fp38 : (L ＼ (* (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* ty))
508 fp38 = SB.not-t (fp02 ty y)
509 fp39 : Union (* ty) ⊆ (* (SB.i (fp02 ty y)))
510 fp39 {w} tyw with ∨L＼X {L} {* (SB.i (fp02 ty y))} (fp40 y tyw)
511 ... | case1 sb = sb
512 ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw )
472 fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) 513 fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
473 fp04 {tx} {ty} = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where 514 fp04 {tx} {ty} = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where
474 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x 515 fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x
475 fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt 516 fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt
476 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫ where 517 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫ where