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

comparison src/Topology.agda @ 1108:720aff4a7fa4

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 Sat, 31 Dec 2022 11:18:04 +0900
parents f4c398c60c67
children f46a16cebbab
comparison
equal deleted inserted replaced
1107:f4c398c60c67 1108:720aff4a7fa4
43 -- closed Set 43 -- closed Set
44 CS : HOD 44 CS : HOD
45 CS = record { od = record { def = λ x → odef OS (& ( L ＼ (* x ))) } ; odmax = & L ; <odmax = tp02 } where 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 46 tp02 : {y : Ordinal } → odef OS (& (L ＼ * y)) → y o< & L
47 tp02 {y} nop = ? 47 tp02 {y} nop = ?
48 os⊆L : {x : HOD} → OS ∋ x → x ⊆ L
49 os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy )
48 -- ∈∅< ( proj1 nop ) 50 -- ∈∅< ( proj1 nop )
49 51
50 open Topology 52 open Topology
51 53
52 -- Base 54 -- Base
55 57
56 data Subbase (P : HOD) : Ordinal → Set n where 58 data Subbase (P : HOD) : Ordinal → Set n where
57 gi : {x : Ordinal } → odef P x → Subbase P x 59 gi : {x : Ordinal } → odef P x → Subbase P x
58 g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) 60 g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y))
59 61
60 Subases : (P : HOD) → HOD 62 Subbases : (P : HOD) → HOD
61 Subases P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ; <odmax = ? } 63 Subbases P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ; <odmax = ? }
62 64
63 record Base (P : HOD) (x : Ordinal) : Set n where 65 record Base (P : HOD) (x : Ordinal) : Set n where
64 field 66 field
65 b : Ordinal 67 b : Ordinal
66 pb : odef (Power (Subases P) ) b 68 pb : odef (Power (Subbases P) ) b
67 union : odef (Union (* b)) x 69 bx : odef (* b) x
68 70
69 GeneratedTop : (P : HOD) → HOD 71 GeneratedTop : (P : HOD) → HOD
70 GeneratedTop P = record { od = record { def = λ x → Base P x } ; odmax = & P ; <odmax = ? } 72 GeneratedTop P = record { od = record { def = λ x → Base P x } ; odmax = & P ; <odmax = ? }
71 73
72 -- covers 74 -- covers
130 base : {P Q : HOD} → Topology P → Topology Q → HOD 132 base : {P Q : HOD} → Topology P → Topology Q → HOD
131 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? } 133 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
132 134
133 POS : {P Q : HOD} → Topology P → Topology Q → HOD 135 POS : {P Q : HOD} → Topology P → Topology Q → HOD
134 POS {P} {Q} TP TQ = GeneratedTop (base TP TQ) 136 POS {P} {Q} TP TQ = GeneratedTop (base TP TQ)
137
135 138
136 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) 139 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
137 _Top⊗_ {P} {Q} TP TQ = record { 140 _Top⊗_ {P} {Q} TP TQ = record {
138 OS = POS TP TQ 141 OS = POS TP TQ
139 ; OS⊆PL = tp10 142 ; OS⊆PL = tp10
140 ; o∪ = ? 143 ; o∪ = tp13
141 ; o∩ = ? 144 ; o∩ = ?
142 } where 145 } where
143 -- B : (OS P ∋ x → proj⁻¹ x ) ∨ (OS Q ∋ y → proj⁻¹ y ) 146 -- B : (OS P ∋ x → proj⁻¹ x ) ∨ (OS Q ∋ y → proj⁻¹ y )
144 -- U ⊂ ZFP P Q ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧ b ⊂ U ) 147 -- U ⊂ ZFP P Q ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧ b ⊂ U )
145 tp11 : {x y z : Ordinal } → Subbase (base TP TQ) y → odef (* y) x → odef (* x) z → ZFProduct P Q z 148 tp11 : {x z : Ordinal } → Subbase (base TP TQ) z → odef (* z) x → ZFProduct P Q x
146 tp11 {x} {y} {z} (gi (case1 record { p = p ; q = q ; op = op ; prod = prod })) yx xz = ? 149 tp11 {x} {z} (gi (case1 record { p = p ; q = q ; op = op ; prod = z=zfp })) zx = tp12 where
147 tp11 {x} {y} {z} (gi (case2 bp)) yx xz = ? 150 tp12 : ZFProduct P Q x
148 tp11 {x} (g∩ {a} {b} sb sb₁) yx xz = tp11 {x} {a} sb (proj1 (subst (λ k → odef k x) *iso yx)) xz 151 tp12 with subst (λ k → odef k x) (trans (cong (*) z=zfp) *iso) zx
152 ... | ab-pair pa qb = ZFP→
153 (os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op ) (subst (λ k → odef (* p) k) (sym &iso) pa) )
154 (subst (λ k → odef Q k ) (sym &iso) qb )
155 tp11 {x} {z} (gi (case2 record { p = p ; q = q ; oq = oq ; prod = z=zfp })) zx = tp12 where
156 tp12 : ZFProduct P Q x
157 tp12 with subst (λ k → odef k x) (trans (cong (*) z=zfp) *iso) zx
158 ... | ab-pair pa qb = ZFP→
159 (subst (λ k → odef P k ) (sym &iso) pa )
160 ((os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq )) (subst (λ k → odef (* q) k) (sym &iso) qb) )
161 tp11 {x} (g∩ {a} {b} sb sb₁) zx = tp11 sb (proj1 (subst (λ k → odef k x) *iso zx ))
149 tp10 : POS TP TQ ⊆ Power (ZFP P Q) 162 tp10 : POS TP TQ ⊆ Power (ZFP P Q)
150 tp10 {x} record { b = b ; pb = pb ; union = record { owner = y ; ao = by ; ox = yx } } z xz = tp11 (pb _ by) yx xz 163 tp10 {x} record { b = b ; pb = pb ; bx = bx } z xz = tp11 (pb _ bx) xz
164 tp13 : {U : HOD} → U ⊆ POS TP TQ → POS TP TQ ∋ Union U
165 tp13 {U} U⊆O = record { b = ? ; pb = ? ; bx = ? }
151 166
152 -- existence of Ultra Filter 167 -- existence of Ultra Filter
153 168
154 open Filter 169 open Filter
155 170