|
431
|
1 open import Level
|
|
|
2 open import Ordinals
|
|
|
3 module Topology {n : Level } (O : Ordinals {n}) where
|
|
|
4
|
|
|
5 open import zf
|
|
|
6 open import logic
|
|
|
7 open _∧_
|
|
|
8 open _∨_
|
|
|
9 open Bool
|
|
|
10
|
|
|
11 import OD
|
|
|
12 open import Relation.Nullary
|
|
|
13 open import Data.Empty
|
|
|
14 open import Relation.Binary.Core
|
|
|
15 open import Relation.Binary.PropositionalEquality
|
|
|
16 import BAlgbra
|
|
|
17 open BAlgbra O
|
|
|
18 open inOrdinal O
|
|
|
19 open OD O
|
|
|
20 open OD.OD
|
|
|
21 open ODAxiom odAxiom
|
|
|
22 import OrdUtil
|
|
|
23 import ODUtil
|
|
|
24 open Ordinals.Ordinals O
|
|
|
25 open Ordinals.IsOrdinals isOrdinal
|
|
|
26 open Ordinals.IsNext isNext
|
|
|
27 open OrdUtil O
|
|
|
28 open ODUtil O
|
|
|
29
|
|
|
30 import ODC
|
|
|
31 open ODC O
|
|
|
32
|
|
|
33 open import filter
|
|
1101
|
34 open import OPair O
|
|
|
35
|
|
431
|
36
|
|
482
|
37 record Topology ( L : HOD ) : Set (suc n) where
|
|
431
|
38 field
|
|
|
39 OS : HOD
|
|
|
40 OS⊆PL : OS ⊆ Power L
|
|
|
41 o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P
|
|
|
42 o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q)
|
|
1101
|
43 -- closed Set
|
|
|
44 CS : HOD
|
|
|
45 CS = record { od = record { def = λ x → odef OS (& ( L ＼ (* x ))) } ; odmax = & L ; <odmax = tp02 } where
|
|
|
46 tp02 : {y : Ordinal } → odef OS (& (L ＼ * y)) → y o< & L
|
|
|
47 tp02 {y} nop = ?
|
|
|
48 -- ∈∅< ( proj1 nop )
|
|
431
|
49
|
|
482
|
50 open Topology
|
|
431
|
51
|
|
1101
|
52
|
|
431
|
53 record _covers_ ( P q : HOD ) : Set (suc n) where
|
|
|
54 field
|
|
|
55 cover : {x : HOD} → q ∋ x → HOD
|
|
|
56 P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
|
|
|
57 isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x
|
|
|
58
|
|
|
59 -- Base
|
|
|
60 -- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that
|
|
|
61 -- W ⊆ U ∩ V and x ∈ W .
|
|
|
62
|
|
|
63 data genTop (P : HOD) : HOD → Set (suc n) where
|
|
|
64 gi : {x : HOD} → P ∋ x → genTop P x
|
|
|
65 g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y)
|
|
|
66 g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q)
|
|
|
67
|
|
|
68 -- Limit point
|
|
|
69
|
|
1101
|
70 record LP { L : HOD} (top : Topology L) ( S x : HOD ) (S⊆PL : S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where
|
|
431
|
71 field
|
|
|
72 neip : {y : HOD} → OS top ∋ y → y ∋ x → HOD
|
|
|
73 isNeip : {y : HOD} → (o∋y : OS top ∋ y ) → (y∋x : y ∋ x ) → ¬ ( x ≡ neip o∋y y∋x) ∧ ( y ∋ neip o∋y y∋x )
|
|
|
74
|
|
|
75 -- Finite Intersection Property
|
|
|
76
|
|
|
77 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
|
|
1101
|
78 fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
|
|
|
79 fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
|
|
431
|
80
|
|
1101
|
81 record FIP {L : HOD} (top : Topology L) ( P : HOD ) : Set (suc n) where
|
|
431
|
82 field
|
|
1101
|
83 fipS⊆PL : P ⊆ CS top
|
|
431
|
84 fip≠φ : { x : HOD } → Finite-∩ P x → ¬ ( x ≡ od∅ )
|
|
|
85
|
|
|
86 -- Compact
|
|
|
87
|
|
|
88 data Finite-∪ (S : HOD) : HOD → Set (suc n) where
|
|
1101
|
89 fin-e : {x : HOD} → S ∋ x → Finite-∪ S x
|
|
431
|
90 fin-∪ : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
|
|
|
91
|
|
1101
|
92 record Compact {L : HOD} (top : Topology L) ( P : HOD ) : Set (suc n) where
|
|
431
|
93 field
|
|
1101
|
94 finCover : {X : HOD} → X ⊆ OS top → X covers P → HOD
|
|
|
95 isFinCover : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → (finCover xo xcp ) covers P
|
|
|
96 isFiniteCover : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → Finite-∪ X (finCover xo xcp )
|
|
431
|
97
|
|
|
98 -- FIP is Compact
|
|
|
99
|
|
1101
|
100 FIP→Compact : {L P : HOD} → (top : Topology L ) → FIP top P → Compact top P
|
|
|
101 FIP→Compact {L} {P} TL fip = record { finCover = ? ; isFinCover = ? ; isFiniteCover = ? }
|
|
431
|
102
|
|
1101
|
103 Compact→FIP : {L P : HOD} → (top : Topology L ) → Compact top P → FIP top P
|
|
482
|
104 Compact→FIP = {!!}
|
|
431
|
105
|
|
|
106 -- Product Topology
|
|
|
107
|
|
1101
|
108 open ZFProduct
|
|
|
109
|
|
|
110 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
|
|
|
111 _Top⊗_ {P} {Q} TP TQ = record {
|
|
|
112 OS = POS
|
|
|
113 ; OS⊆PL = ?
|
|
|
114 ; o∪ = ?
|
|
|
115 ; o∩ = ?
|
|
|
116 } where
|
|
|
117 box : HOD
|
|
|
118 box = ZFP (OS TP) (OS TQ)
|
|
|
119 POS : HOD
|
|
|
120 POS = ?
|
|
431
|
121
|
|
|
122 -- existence of Ultra Filter
|
|
|
123
|
|
|
124 -- Ultra Filter has limit point
|
|
|
125
|
|
|
126 -- FIP is UFL
|
|
|
127
|
|
|
128 -- Product of UFL has limit point (Tychonoff)
|
|
|
129
|
