Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/Topology.agda @ 1191:d969fc17d049
fix FIP again
author | kono |
---|---|
date | Mon, 27 Feb 2023 08:26:35 +0800 |
parents | e110b56d8cbe |
children | 2c35ccd5aadd |
comparison
equal
deleted
inserted
replaced
1190:e110b56d8cbe | 1191:d969fc17d049 |
---|---|
262 | 262 |
263 open _covers_ | 263 open _covers_ |
264 | 264 |
265 -- Finite Intersection Property | 265 -- Finite Intersection Property |
266 | 266 |
267 data Finite-∩ (S : HOD) : Ordinal → Set n where | |
268 fin-e : Finite-∩ S o∅ | |
269 fin-i : {x : Ordinal } → odef S x → Finite-∩ S (& ( * x , * x )) | |
270 fin-∩ : {x y : Ordinal } → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (& (* x ∩ * y)) | |
271 | |
267 record FIP {L : HOD} (top : Topology L) : Set n where | 272 record FIP {L : HOD} (top : Topology L) : Set n where |
268 field | 273 field |
269 limit : {X : Ordinal } → * X ⊆ CS top | 274 limit : {X : Ordinal } → * X ⊆ CS top |
270 → ( { x : Ordinal } → Subbase (* X) x → o∅ o< x ) → Ordinal | 275 → ( { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) → Ordinal |
271 is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) | 276 is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) |
272 → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x ) | 277 → ( fip : { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) |
273 → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip) | 278 → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip) |
274 L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) | 279 L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) |
275 → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x ) | 280 → ( fip : { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) |
276 → {x : Ordinal } → odef (* X) x | 281 → {x : Ordinal } → odef (* X) x |
277 → odef L (limit CX fip) | 282 → odef L (limit CX fip) |
278 L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx) | 283 L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx) |
279 | 284 |
280 -- Compact | 285 -- Compact |
326 -- | 331 -- |
327 -- X covres L means Intersection of (CX X) contains nothing | 332 -- X covres L means Intersection of (CX X) contains nothing |
328 -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP) | 333 -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP) |
329 -- it means there is a finite cover | 334 -- it means there is a finite cover |
330 -- | 335 -- |
331 finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L → Subbase (Replace (* X) (λ z → L \ z)) o∅ | 336 finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L → Finite-∩ (Replace (* X) (λ z → L \ z)) o∅ |
332 finCoverBase {X} ox oc with ODC.p∨¬p O (Subbase (Replace (* X) (λ z → L \ z)) o∅) | 337 finCoverBase {X} ox oc with ODC.p∨¬p O (Finite-∩ (Replace (* X) (λ z → L \ z)) o∅) |
333 ... | case1 sb = sb | 338 ... | case1 sb = sb |
334 ... | case2 ¬sb = ⊥-elim (fip09 fip25 fip20) where | 339 ... | case2 ¬sb = ⊥-elim (fip09 fip25 fip20) where |
335 fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) | 340 fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) |
336 fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ )) | 341 fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ )) |
337 -- CX is finite intersection | 342 -- CX is finite intersection |
338 fip02 : {x : Ordinal} → Subbase (* (CX ox)) x → o∅ o< x | 343 fip02 : {x : Ordinal} → Finite-∩ (* (CX ox)) x → o∅ o< x |
339 fip02 {x} sc with trio< x o∅ | 344 fip02 {x} sc with trio< x o∅ |
340 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | 345 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
341 ... | tri> ¬a ¬b c = c | 346 ... | tri> ¬a ¬b c = c |
342 ... | tri≈ ¬a b ¬c = ⊥-elim (¬sb (subst₂ (λ j k → Subbase j k ) *iso b sc )) | 347 ... | tri≈ ¬a b ¬c = ⊥-elim (¬sb (subst₂ (λ j k → Finite-∩ j k ) *iso b sc )) |
343 -- we have some intersection because L is not empty (if we have an element of L, we don't need choice) | 348 -- we have some intersection because L is not empty (if we have an element of L, we don't need choice) |
344 fip26 : odef (* (CX ox)) (& (L \ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) ))) | 349 fip26 : odef (* (CX ox)) (& (L \ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) ))) |
345 fip26 = subst (λ k → odef k (& (L \ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso) | 350 fip26 = subst (λ k → odef k (& (L \ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso) |
346 record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L)) ; x=ψz = refl } | 351 record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L)) ; x=ψz = refl } |
347 fip25 : odef L( FIP.limit fip (CCX ox) fip02 ) | 352 fip25 : odef L( FIP.limit fip (CCX ox) fip02 ) |
350 fip20 {y} Xy yl = proj2 fip21 yl where | 355 fip20 {y} Xy yl = proj2 fip21 yl where |
351 fip22 : odef (* (CX ox)) (& ( L \ * y )) | 356 fip22 : odef (* (CX ox)) (& ( L \ * y )) |
352 fip22 = subst (λ k → odef k (& ( L \ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } | 357 fip22 = subst (λ k → odef k (& ( L \ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } |
353 fip21 : odef (L \ * y) ( FIP.limit fip (CCX ox) fip02 ) | 358 fip21 : odef (L \ * y) ( FIP.limit fip (CCX ox) fip02 ) |
354 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) | 359 fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) |
355 finCoverSet : {X : Ordinal } → (x : Ordinal) → Subbase (Replace (* X) (λ z → L \ z)) x → HOD | 360 finCoverSet : {X : Ordinal } → (x : Ordinal) → Finite-∩ (Replace (* X) (λ z → L \ z)) x → HOD |
356 finCoverSet {X} x (gi rx) = ( L \ * x ) , ( L \ * x ) | 361 finCoverSet {X} x fin-e = ? |
357 finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy | 362 finCoverSet {X} x (fin-i rx) = ( L \ * x ) , ( L \ * x ) |
363 finCoverSet {X} x∩y (fin-∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy | |
358 -- | 364 -- |
359 -- this defines finite cover | 365 -- this defines finite cover |
360 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal | 366 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal |
361 finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc)) | 367 finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc)) |
362 -- create Finite-∪ from cex | 368 -- create Finite-∪ from cex |
363 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) | 369 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) |
364 isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where | 370 isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where |
365 fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L \ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) | 371 fip60 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L \ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) |
366 fip60 x (gi rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 rx)) where | 372 fip60 x fin-e = ? |
373 fip60 x (fin-i rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 ? )) where | |
367 fip62 : & (* (& (L \ * x)) , * (& (L \ * x))) ≡ & ((L \ * x) , (L \ * x)) | 374 fip62 : & (* (& (L \ * x)) , * (& (L \ * x))) ≡ & ((L \ * x) , (L \ * x)) |
368 fip62 = cong₂ (λ j k → & (j , k )) *iso *iso | 375 fip62 = cong₂ (λ j k → & (j , k )) *iso *iso |
369 fip61 : odef (Replace (* X) (_\_ L)) x → odef (* X) ( & ((L \ * x ) )) | 376 fip61 : odef (Replace (* X) (_\_ L)) x → odef (* X) ( & ((L \ * x ) )) |
370 fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where | 377 fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where |
371 fip34 : * z1 ⊆ L | 378 fip34 : * z1 ⊆ L |
375 z1 ≡⟨ sym &iso ⟩ | 382 z1 ≡⟨ sym &iso ⟩ |
376 & (* z1) ≡⟨ cong (&) (sym (L\Lx=x fip34 )) ⟩ | 383 & (* z1) ≡⟨ cong (&) (sym (L\Lx=x fip34 )) ⟩ |
377 & (L \ ( L \ * z1)) ≡⟨ cong (λ k → & ( L \ k )) (sym *iso) ⟩ | 384 & (L \ ( L \ * z1)) ≡⟨ cong (λ k → & ( L \ k )) (sym *iso) ⟩ |
378 & (L \ * (& ( L \ * z1))) ≡⟨ cong (λ k → & ( L \ * k )) (sym x=ψz1) ⟩ | 385 & (L \ * (& ( L \ * z1))) ≡⟨ cong (λ k → & ( L \ * k )) (sym x=ψz1) ⟩ |
379 & (L \ * x ) ∎ where open ≡-Reasoning | 386 & (L \ * x ) ∎ where open ≡-Reasoning |
380 fip60 x∩y (g∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx) (fip60 y sy) ) where | 387 fip60 x∩y (fin-∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx) (fip60 y sy) ) where |
381 fip62 : & (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡ & (finCoverSet x sx ∪ finCoverSet y sy) | 388 fip62 : & (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡ & (finCoverSet x sx ∪ finCoverSet y sy) |
382 fip62 = cong (&) ( begin | 389 fip62 = cong (&) ( begin |
383 (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ *iso *iso ⟩ | 390 (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ *iso *iso ⟩ |
384 finCoverSet x sx ∪ finCoverSet y sy ∎ ) where open ≡-Reasoning | 391 finCoverSet x sx ∪ finCoverSet y sy ∎ ) where open ≡-Reasoning |
385 -- is also a cover | 392 -- is also a cover |
386 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L | 393 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L |
387 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L \ k ≡ L) (sym o∅≡od∅) L\0=L) | 394 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L \ k ≡ L) (sym o∅≡od∅) L\0=L) |
388 (fip70 o∅ (finCoverBase xo xcp)) where | 395 (fip70 o∅ (finCoverBase xo xcp)) where |
389 fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L \ z)) x ) → (finCoverSet {X} x sb) covers (L \ * x) | 396 fip70 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L \ z)) x ) → (finCoverSet {X} x sb) covers (L \ * x) |
390 fip70 x (gi rx) = record { cover = λ _ → & (L \ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } | 397 fip70 x fin-e = ? |
391 fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers | 398 fip70 x (fin-i rx) = record { cover = λ _ → & (L \ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } |
392 (L \ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} ? ? ) where | 399 fip70 x∩y (fin-∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) ? covers |
400 (L \ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where | |
393 fip45 : {L a b : HOD} → (L \ (a ∩ b)) ⊆ ( (L \ a) ∪ (L \ b)) | 401 fip45 : {L a b : HOD} → (L \ (a ∩ b)) ⊆ ( (L \ a) ∪ (L \ b)) |
394 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x) | 402 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x) |
395 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫ | 403 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫ |
396 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫ | 404 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫ |
405 fip71 : {a b c : HOD} → a covers c → (a ∪ b) covers c | |
406 fip71 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case1 (P∋cover cov lt) | |
407 ; isCover = isCover cov } | |
408 fip72 : {a b c : HOD} → a covers c → (b ∪ a) covers c | |
409 fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt) | |
410 ; isCover = isCover cov } | |
397 fip43 : {A L a b : HOD } → A covers (L \ a) → A covers (L \ b ) → A covers ( L \ ( a ∩ b ) ) | 411 fip43 : {A L a b : HOD } → A covers (L \ a) → A covers (L \ b ) → A covers ( L \ ( a ∩ b ) ) |
398 fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where | 412 fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where |
399 fip44 : {x : Ordinal} → odef (L \ (a ∩ b)) x → Ordinal | 413 fip44 : {x : Ordinal} → odef (L \ (a ∩ b)) x → Ordinal |
400 fip44 {x} Lab with fip45 {L} {a} {b} Lab | 414 fip44 {x} Lab with fip45 {L} {a} {b} Lab |
401 ... | case1 La = cover ca La | 415 ... | case1 La = cover ca La |
426 comp01 = subst (λ k → odef (* X) k) (sym &iso) az | 440 comp01 = subst (λ k → odef (* X) k) (sym &iso) az |
427 | 441 |
428 -- if all finite intersection of X contains something, | 442 -- if all finite intersection of X contains something, |
429 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) | 443 -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) |
430 -- it means there is a limit | 444 -- it means there is a limit |
431 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) | 445 has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x) |
432 → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ ) | 446 → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ ) |
433 has-intersection {X} CX fip 0<X i=0 = ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05 ⟫ )) where | 447 has-intersection {X} CX fip 0<X i=0 = ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05 ⟫ )) where |
434 fp07 : HOD -- we have an element of X | 448 fp07 : HOD -- we have an element of X |
435 fp07 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | 449 fp07 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) |
436 fp08 : odef (* X) (& fp07) | 450 fp08 : odef (* X) (& fp07) |
437 fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) | 451 fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) |
438 no-cover : ¬ ( (* (OX CX)) covers L ) | 452 no-cover : ¬ ( (* (OX CX)) covers L ) |
439 no-cover cov = ⊥-elim ( ? ) where | 453 no-cover cov = ⊥-elim ( ? ) where |
440 fp01 : Ordinal | 454 fp01 : Ordinal |
441 fp01 = Compact.finCover compact (OOX CX) cov | 455 fp01 = Compact.finCover compact (OOX CX) cov |
442 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L \ * t ) ) | 456 fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Finite-∩ (* X) (& ( L \ * t ) ) |
443 fp02 t fin-e = gi ? | 457 fp02 t fin-e = ? |
444 fp02 t (fin-i tx ) = gi fp03 where | 458 fp02 t (fin-i tx ) = ? where |
445 fp03 : odef (* X) (& (L \ * t)) | 459 fp03 : odef (* X) (& (L \ * t)) |
446 fp03 = ? | 460 fp03 = ? |
447 fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (fp02 tx x) (fp02 ty y ) ) where | 461 fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Finite-∩ (* X) k ) fp04 ( fin-∩ (fp02 tx x) (fp02 ty y ) ) where |
448 fp04 : & (* (& (L \ * tx)) ∩ * (& (L \ * ty))) ≡ & (L \ * (& (* tx ∪ * ty))) | 462 fp04 : & (* (& (L \ * tx)) ∩ * (& (L \ * ty))) ≡ & (L \ * (& (* tx ∪ * ty))) |
449 fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where | 463 fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where |
450 fp05 : {x : Ordinal} → odef (* (& (L \ * tx)) ∩ * (& (L \ * ty))) x → odef (L \ * (& (* tx ∪ * ty))) x | 464 fp05 : {x : Ordinal} → odef (* (& (L \ * tx)) ∩ * (& (L \ * ty))) x → odef (L \ * (& (* tx ∪ * ty))) x |
451 fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt | 465 fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt |
452 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L \ k) x) (sym *iso) ⟪ Lx , fp06 ⟫ where | 466 ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L \ k) x) (sym *iso) ⟪ Lx , fp06 ⟫ where |
495 fp06 = begin | 509 fp06 = begin |
496 NC.x not-covered ≡⟨ sym &iso ⟩ | 510 NC.x not-covered ≡⟨ sym &iso ⟩ |
497 & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered fp08)) ⟩ | 511 & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered fp08)) ⟩ |
498 & fp07 <⟨ c<→o< fp08 ⟩ | 512 & fp07 <⟨ c<→o< fp08 ⟩ |
499 & (* X) ∎ where open o≤-Reasoning O | 513 & (* X) ∎ where open o≤-Reasoning O |
500 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) | 514 limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x) |
501 → Ordinal | 515 → Ordinal |
502 limit {X} CX fip with trio< X o∅ | 516 limit {X} CX fip with trio< X o∅ |
503 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | 517 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
504 ... | tri≈ ¬a b ¬c = o∅ | 518 ... | tri≈ ¬a b ¬c = o∅ |
505 ... | tri> ¬a ¬b c = & (ODC.minimal O (Intersection (* X)) ( has-intersection CX fip c)) | 519 ... | tri> ¬a ¬b c = & (ODC.minimal O (Intersection (* X)) ( has-intersection CX fip c)) |
506 fip00 : {X : Ordinal} (CX : * X ⊆ CS top) | 520 fip00 : {X : Ordinal} (CX : * X ⊆ CS top) |
507 (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) | 521 (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x) |
508 {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip ) | 522 {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip ) |
509 fip00 {X} CX fip {x} Xx with trio< X o∅ | 523 fip00 {X} CX fip {x} Xx with trio< X o∅ |
510 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) | 524 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) |
511 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) (subst (λ k → o∅ o< k) &iso (∈∅< Xx) ) ) | 525 ... | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (sym b) (subst (λ k → o∅ o< k) &iso (∈∅< Xx) ) ) |
512 ... | tri> ¬a ¬b c with ODC.x∋minimal O (Intersection (* X)) ( has-intersection CX fip c ) | 526 ... | tri> ¬a ¬b c with ODC.x∋minimal O (Intersection (* X)) ( has-intersection CX fip c ) |