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

comparison src/Topology.agda @ 1110:7fb6950b50f1

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 19:30:54 +0900
parents f46a16cebbab
children b77a7f724663
comparison
equal deleted inserted replaced
1109:f46a16cebbab 1110:7fb6950b50f1
69 bx : odef (* b) x 69 bx : odef (* b) x
70 70
71 GeneratedTop : (P : HOD) → HOD 71 GeneratedTop : (P : HOD) → HOD
72 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 = ? }
73 73
74 record IsBase (L P : HOD) : Set (suc n) where
75 field
76 p : {x : HOD} → L ∋ x → HOD
77 in-P : {x : HOD} → (lx : L ∋ x ) → P ∋ p lx
78 b∩ : {x y : HOD} → (bx : P ∋ x ) (by : P ∋ y ) → HOD
79 b∩⊂ : {x y z : HOD} → {bx : P ∋ x } {by : P ∋ y } → ( x ∩ y ) ∋ z → ( b∩ bx by ∋ x ) ∧ ( b∩ bx by ⊆ ( x ∩ y ) )
80
81 GeneratedIsTopogy : (P L : HOD) → IsBase L P → Topology L
82 GeneratedIsTopogy = ?
83
74 -- covers 84 -- covers
75 85
76 record _covers_ ( P q : HOD ) : Set (suc n) where 86 record _covers_ ( P q : HOD ) : Set (suc n) where
77 field 87 field
78 cover : {x : HOD} → q ∋ x → HOD 88 cover : {x : HOD} → q ∋ x → HOD
133 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? } 143 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
134 144
135 POS : {P Q : HOD} → Topology P → Topology Q → HOD 145 POS : {P Q : HOD} → Topology P → Topology Q → HOD
136 POS {P} {Q} TP TQ = GeneratedTop (base TP TQ) 146 POS {P} {Q} TP TQ = GeneratedTop (base TP TQ)
137 147
148 PU : {A B : HOD} → Power A ∋ B → Power A ∋ Union B
149 PU = ?
138 150
139 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) 151 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
140 _Top⊗_ {P} {Q} TP TQ = record { 152 _Top⊗_ {P} {Q} TP TQ = record {
141 OS = POS TP TQ 153 OS = POS TP TQ
142 ; OS⊆PL = tp10 154 ; OS⊆PL = tp10
162 tp10 : POS TP TQ ⊆ Power (ZFP P Q) 174 tp10 : POS TP TQ ⊆ Power (ZFP P Q)
163 tp10 {x} record { b = b ; pb = pb ; bx = bx } z xz = tp11 (pb _ bx) xz 175 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 176 tp13 : {U : HOD} → U ⊆ POS TP TQ → POS TP TQ ∋ Union U
165 tp13 {U} U⊆O = tp20 U U⊆O where 177 tp13 {U} U⊆O = tp20 U U⊆O where
166 ind : {x : HOD} → ({y : HOD} → x ∋ y → y ⊆ POS TP TQ → POS TP TQ ∋ Union y) → x ⊆ POS TP TQ → POS TP TQ ∋ Union x 178 ind : {x : HOD} → ({y : HOD} → x ∋ y → y ⊆ POS TP TQ → POS TP TQ ∋ Union y) → x ⊆ POS TP TQ → POS TP TQ ∋ Union x
167 ind {x} prev x⊆O = record { b = ? ; pb = ? ; bx = ? } 179 ind {x} prev x⊆O = record { b = & ub ; pb = ? ; bx = ? } where
180 ub : HOD
181 ub = Union ( Replace' x ( λ z xz → * (Base.b (x⊆O xz) ) ) )
182 tp14 : ub ∋ Union x
183 tp14 = ?
168 tp20 : (U : HOD ) → U ⊆ POS TP TQ → POS TP TQ ∋ Union U 184 tp20 : (U : HOD ) → U ⊆ POS TP TQ → POS TP TQ ∋ Union U
169 tp20 U U⊆O = ε-induction0 { λ U → U ⊆ POS TP TQ → POS TP TQ ∋ Union U } ind U U⊆O 185 tp20 U U⊆O = ε-induction0 { λ U → U ⊆ POS TP TQ → POS TP TQ ∋ Union U } ind U U⊆O
170 tp14 : {p q : HOD} → POS TP TQ ∋ p → POS TP TQ ∋ q → POS TP TQ ∋ (p ∩ q) 186 tp14 : {p q : HOD} → POS TP TQ ∋ p → POS TP TQ ∋ q → POS TP TQ ∋ (p ∩ q)
171 tp14 {p} {q} op oq = record { b = & tp15 ; pb = ? ; bx = ? } where 187 tp14 {p} {q} op oq = record { b = & tp15 ; pb = ? ; bx = ? } where
172 tp15 : HOD 188 tp15 : HOD