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

comparison src/Topology.agda @ 1153:5eb972738f9b

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 Wed, 18 Jan 2023 14:09:53 +0900
parents e1c6719a8c38
children 0612874b815c
comparison
equal deleted inserted replaced
1152:e1c6719a8c38 1153:5eb972738f9b
393 & (L ＼ * y ) 393 & (L ＼ * y )
394 ∎ where open ≡-Reasoning 394 ∎ where open ≡-Reasoning
395 fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w 395 fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w
396 fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw 396 fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
397 397
398
399
400 -- some day 398 -- some day
401 Compact→FIP : Set (suc n) 399 Compact→FIP : Set (suc n)
402 Compact→FIP = {L : HOD} → (top : Topology L ) → Compact top → FIP top 400 Compact→FIP = {L : HOD} → (top : Topology L ) → Compact top → FIP top
403 401
404 -- existence of Ultra Filter 402 -- existence of Ultra Filter
413 limit : Ordinal 411 limit : Ordinal
414 P∋limit : odef P limit 412 P∋limit : odef P limit
415 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F 413 is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F
416 414
417 -- FIP is UFL 415 -- FIP is UFL
416
417 record NFIP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (X : Ordinal) : Set n where
418 field
419 osx : * X ⊆ OS TP
420 fip : {u x : Ordinal} → * u ⊆ (L ＼ * X) → Subbase (* u) x → o∅ o< x
418 421
419 UFLP→FIP : {P : HOD} (TP : Topology P) → {L : HOD} (LP : L ⊆ Power P ) → 422 UFLP→FIP : {P : HOD} (TP : Topology P) → {L : HOD} (LP : L ⊆ Power P ) →
420 ( (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP 423 ( (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP
421 UFLP→FIP {P} TP {L} LP uflp = record { limit = uf00 ; is-limit = {!!} } where 424 UFLP→FIP {P} TP {L} LP uflp = record { limit = uf00 ; is-limit = {!!} } where
422 fip : {X : Ordinal} → * X ⊆ CS TP → Set n 425 fip : {X : Ordinal} → * X ⊆ CS TP → Set n
423 fip {X} CSX = {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x 426 fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
424 N : {X : Ordinal} → (CSX : * X ⊆ CS TP ) → fip {X} CSX → HOD 427 N : HOD
425 N {X} CSX fip = record { od = record { def = λ x → Base L P X x ∧ ( o∅ o< x ) } ; odmax = ? ; <odmax = ? } 428 N = record { od = record { def = λ X → NFIP TP LP X } ; odmax = ? ; <odmax = ? }
426 F : {X : Ordinal} → (CSX : * X ⊆ CS TP ) → fip {X} CSX → Filter {L} {P} LP 429 F : Filter {L} {P} LP
427 F {X} CSX fip = record { filter = N CSX fip ; f⊆L = ? ; filter1 = ? ; filter2 = ? } 430 F = record { filter = N ; f⊆L = ? ; filter1 = f1 ; filter2 = ? } where
431 f1 : {p q : HOD} → L ∋ q → N ∋ p → p ⊆ q → N ∋ q
432 f1 {p} {q} Lq record { osx = osx ; fip = fip } p⊆q = record { osx = ? ; fip = ? }
428 uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal 433 uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
429 uf00 {X} CSX fip = UFLP.limit ( uflp 434 uf00 {X} CSX fip = ?
430 ( MaximumFilter.mf (F→Maximum {L} {P} LP ? ? (F CSX ?) ? ? ? )) 435 -- UFLP.limit ( uflp
431 ? 436 -- ( MaximumFilter.mf (F→Maximum {L} {P} LP ? ? (F CSX ?) ? ? ? ))
432 (F→ultra LP ? ? (F CSX fip) ? ? ? ) ) 437 -- ?
438 -- (F→ultra LP ? ? (F CSX fip) ? ? ? ) )
433 439
434 -- some day 440 -- some day
435 FIP→UFLP : Set (suc (suc n)) 441 FIP→UFLP : Set (suc (suc n))
436 FIP→UFLP = {P : HOD} (TP : Topology P) → FIP TP 442 FIP→UFLP = {P : HOD} (TP : Topology P) → FIP TP
437 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F FP UF 443 → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F FP UF