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

comparison src/Topology.agda @ 1145:f8c3537e68a6

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 Mon, 16 Jan 2023 02:22:03 +0900
parents 73b256c5474b
children 1966127fc14f
comparison
equal deleted inserted replaced
1144:73b256c5474b 1145:f8c3537e68a6
204 -- covers 204 -- covers
205 205
206 record _covers_ ( P q : HOD ) : Set n where 206 record _covers_ ( P q : HOD ) : Set n where
207 field 207 field
208 cover : {x : Ordinal } → odef q x → Ordinal 208 cover : {x : Ordinal } → odef q x → Ordinal
209 P∋cover : {x : Ordinal } → {lt : odef q x} → odef P (cover lt) 209 P∋cover : {x : Ordinal } → (lt : odef q x) → odef P (cover lt)
210 isCover : {x : Ordinal } → {lt : odef q x} → odef (* (cover lt)) x 210 isCover : {x : Ordinal } → (lt : odef q x) → odef (* (cover lt)) x
211 211
212 open _covers_ 212 open _covers_
213 213
214 -- Finite Intersection Property 214 -- Finite Intersection Property
215 215
278 Cex = record { od = record { def = λ x → CFIP x } ; odmax = osuc (& (CS top)) ; <odmax = λ {x} lt → 278 Cex = record { od = record { def = λ x → CFIP x } ; odmax = osuc (& (CS top)) ; <odmax = λ {x} lt →
279 subst₂ (λ j k → j o≤ k ) &iso refl ( ⊆→o≤ (CFIP.is-CS lt )) } 279 subst₂ (λ j k → j o≤ k ) &iso refl ( ⊆→o≤ (CFIP.is-CS lt )) }
280 cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal 280 cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
281 cex {X} ox oc = & ( ODC.minimal O Cex fip00) where 281 cex {X} ox oc = & ( ODC.minimal O Cex fip00) where
282 fip00 : ¬ ( Cex =h= od∅ ) 282 fip00 : ¬ ( Cex =h= od∅ )
283 fip00 cex=0 = fip03 (FIP.is-limit fip (CCX ox) fip02 fip07 ) fip09 where 283 fip00 cex=0 = ⊥-elim (fip09 fip25 fip20) where
284 fip03 : {x z : Ordinal } → odef (* x) z → (¬ odef (* x) z) → ⊥ 284 fip03 : {x z : Ordinal } → odef (* x) z → (¬ odef (* x) z) → ⊥
285 fip03 {x} {z} xz nxz = nxz xz 285 fip03 {x} {z} xz nxz = nxz xz
286 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x 286 fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
287 fip02 {C} {x} C<CX sc with trio< x o∅ 287 fip02 {C} {x} C<CX sc with trio< x o∅
288 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) 288 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
289 ... | tri> ¬a ¬b c = c 289 ... | tri> ¬a ¬b c = c
290 ... | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; y = C ; sy = subst (λ k → Subbase (* C) k) b sc } )) where 290 ... | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; y = C ; sy = subst (λ k → Subbase (* C) k) b sc } )) where
291 fip10 : * C ⊆ CS top 291 fip10 : * C ⊆ CS top
292 fip10 {w} cw = CCX ox ( C<CX cw ) 292 fip10 {w} cw = CCX ox ( C<CX cw )
293 fip01 : Ordinal 293 fip25 : odef L( FIP.limit fip (CCX ox) fip02 )
294 fip01 = FIP.limit fip (CCX ox) fip02 294 fip25 = FIP.L∋limit fip (CCX ox) fip02 ?
295 fip11 : {w : Ordinal } → {Lw : odef L w} → ¬ ( odef (* (cover oc Lw)) w ) 295 fip20 : {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 ))
296 fip11 {w} {Lw} pw = ? where 296 fip20 {y} Xy yl = proj2 fip21 yl where
297 fip15 : odef (* X) (cover oc Lw) 297 fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
298 fip15 = P∋cover oc {w} {Lw} 298 fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl }
299 fip13 : HOD 299 fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 )
300 fip13 = L ＼ * w 300 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 )
301 fip14 : odef (* (CX ox)) (& ( L ＼ * w )) 301 fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z ))
302 fip14 = ? 302 fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
303 fip12 : odef ( L ＼ * w ) fip01
304 fip12 = subst (λ k → odef k fip01 ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip14 )
305 fip10 : odef ? fip01
306 fip10 = FIP.is-limit fip (CCX ox) fip02 ?
307 fip08 : odef L fip01
308 fip08 = FIP.L∋limit fip (CCX ox) fip02 ?
309 fip05 : odef (CS top) fip01
310 fip05 = ?
311 fip07 : odef (* (CX ox)) ( cover oc fip08 )
312 fip07 = ?
313 fip09 : ¬ odef (* (cover oc fip08)) (FIP.limit fip (CCX ox) fip02)
314 fip09 = ?
315 fip04 : Ordinal
316 fip04 = cover oc (cs⊆L top (subst₂ (λ j k → odef j k ) refl (sym &iso) fip05) (FIP.is-limit fip (CCX ox) ? ?) )
317 ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ 303 ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅
318 ¬CXfip {X} ox oc = {!!} where 304 ¬CXfip {X} ox oc = {!!} where
319 fip04 : odef Cex (cex ox oc) 305 fip04 : odef Cex (cex ox oc)
320 fip04 = {!!} 306 fip04 = {!!}
321 -- this defines finite cover 307 -- this defines finite cover