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

comparison src/Topology.agda @ 1109:f46a16cebbab

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 17:56:01 +0900
parents 720aff4a7fa4
children 7fb6950b50f1
comparison
equal deleted inserted replaced
1108:720aff4a7fa4 1109:f46a16cebbab
139 _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)
140 _Top⊗_ {P} {Q} TP TQ = record { 140 _Top⊗_ {P} {Q} TP TQ = record {
141 OS = POS TP TQ 141 OS = POS TP TQ
142 ; OS⊆PL = tp10 142 ; OS⊆PL = tp10
143 ; o∪ = tp13 143 ; o∪ = tp13
144 ; o∩ = ? 144 ; o∩ = tp14
145 } where 145 } where
146 -- B : (OS P ∋ x → proj⁻¹ x ) ∨ (OS Q ∋ y → proj⁻¹ y ) 146 -- B : (OS P ∋ x → proj⁻¹ x ) ∨ (OS Q ∋ y → proj⁻¹ y )
147 -- 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 )
148 tp11 : {x z : Ordinal } → Subbase (base TP TQ) z → odef (* z) x → ZFProduct P Q x 148 tp11 : {x z : Ordinal } → Subbase (base TP TQ) z → odef (* z) x → ZFProduct P Q x
149 tp11 {x} {z} (gi (case1 record { p = p ; q = q ; op = op ; prod = z=zfp })) zx = tp12 where 149 tp11 {x} {z} (gi (case1 record { p = p ; q = q ; op = op ; prod = z=zfp })) zx = tp12 where
160 ((os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq )) (subst (λ k → odef (* q) k) (sym &iso) qb) ) 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 )) 161 tp11 {x} (g∩ {a} {b} sb sb₁) zx = tp11 sb (proj1 (subst (λ k → odef k x) *iso zx ))
162 tp10 : POS TP TQ ⊆ Power (ZFP P Q) 162 tp10 : POS TP TQ ⊆ Power (ZFP P Q)
163 tp10 {x} record { b = b ; pb = pb ; bx = bx } z xz = tp11 (pb _ bx) 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 164 tp13 : {U : HOD} → U ⊆ POS TP TQ → POS TP TQ ∋ Union U
165 tp13 {U} U⊆O = record { b = ? ; pb = ? ; bx = ? } 165 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
167 ind {x} prev x⊆O = record { b = ? ; pb = ? ; bx = ? }
168 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
170 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
172 tp15 : HOD
173 tp15 = ?
166 174
167 -- existence of Ultra Filter 175 -- existence of Ultra Filter
168 176
169 open Filter 177 open Filter
170 178
214 LQ : HOD 222 LQ : HOD
215 LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) 223 LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
216 LQQ : LQ ⊆ Power Q 224 LQQ : LQ ⊆ Power Q
217 LQQ = ? 225 LQQ = ?
218 226
219
220
221
222
223