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

comparison src/Topology.agda @ 1172:f4bccbe80540

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 Sun, 22 Jan 2023 22:41:13 +0900
parents b2ca37e81ad0
children 7d2bae0ff36b
comparison
equal deleted inserted replaced
1171:a839fccdef47 1172:f4bccbe80540
218 -- Product Topology is not 218 -- Product Topology is not
219 -- ZFP (OS TP) (OS TQ) (box) 219 -- ZFP (OS TP) (OS TQ) (box)
220 220
221 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where 221 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
222 field 222 field
223 p q : Ordinal 223 p : Ordinal
224 op : odef (OS TP) p 224 op : odef (OS TP) p
225 prod : x ≡ & (ZFP (* p) Q ) 225 prod : x ≡ & (ZFP (* p) Q )
226 226
227 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where 227 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
228 field 228 field
229 p q : Ordinal 229 q : Ordinal
230 oq : odef (OS TQ) q 230 oq : odef (OS TQ) q
231 prod : x ≡ & (ZFP P (* q )) 231 prod : x ≡ & (ZFP P (* q ))
232 232
233 pbase⊆PL : {P Q : HOD} → (TP : Topology P) → (TQ : Topology Q) → {x : Ordinal } → BaseP TP Q x ∨ BaseQ P TQ x → odef (Power (ZFP P Q)) x 233 pbase⊆PL : {P Q : HOD} → (TP : Topology P) → (TQ : Topology Q) → {x : Ordinal } → BaseP TP Q x ∨ BaseQ P TQ x → odef (Power (ZFP P Q)) x
234 pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; q = q ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where 234 pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where
235 tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q)) 235 tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q))
236 tp01 w wz with subst (λ k → odef k w ) *iso wz 236 tp01 w wz with subst (λ k → odef k w ) *iso wz
237 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where 237 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where
238 tp03 : odef P a 238 tp03 : odef P a
239 tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa 239 tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa
240 pbase⊆PL {P} {Q} TP TQ {z} (case2 record { p = p ; q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where 240 pbase⊆PL {P} {Q} TP TQ {z} (case2 record { q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where
241 tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) )) 241 tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) ))
242 tp01 w wz with subst (λ k → odef k w ) *iso wz 242 tp01 w wz with subst (λ k → odef k w ) *iso wz
243 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where 243 ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where
244 tp03 : odef Q b 244 tp03 : odef Q b
245 tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb 245 tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb