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

comparison src/Topology.agda @ 1190:e110b56d8cbe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author kono
date Mon, 27 Feb 2023 07:29:11 +0800
parents 0201827b08ac
children d969fc17d049 6174001ba1c0
comparison
equal deleted inserted replaced
1189:0201827b08ac 1190:e110b56d8cbe
279 279
280 -- Compact 280 -- Compact
281 281
282 data Finite-∪ (S : HOD) : Ordinal → Set n where 282 data Finite-∪ (S : HOD) : Ordinal → Set n where
283 fin-e : Finite-∪ S o∅ 283 fin-e : Finite-∪ S o∅
284 fin-i : {x : Ordinal } → odef S x → Finite-∪ S x 284 fin-i : {x : Ordinal } → odef S x → Finite-∪ S (& ( * x , * x ))
285 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) 285 fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
286 286
287 record Compact {L : HOD} (top : Topology L) : Set n where 287 record Compact {L : HOD} (top : Topology L) : Set n where
288 field 288 field
289 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal 289 finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal
351 fip22 : odef (* (CX ox)) (& ( L ＼ * y )) 351 fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
352 fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } 352 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 ) 353 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 ) 354 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 355 finCoverSet : {X : Ordinal } → (x : Ordinal) → Subbase (Replace (* X) (λ z → L ＼ z)) x → HOD
356 finCoverSet {X} x (gi rx) = L ＼ * x 356 finCoverSet {X} x (gi rx) = ( L ＼ * x ) , ( L ＼ * x )
357 finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy 357 finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy
358 -- 358 --
359 -- this defines finite cover 359 -- this defines finite cover
360 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal 360 finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
361 finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc)) 361 finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc))
362 -- create Finite-∪ from cex 362 -- create Finite-∪ from cex
363 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) 363 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 364 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)) 365 fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb))
366 fip60 x (gi rx) = fin-i (fip61 rx) where 366 fip60 x (gi rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 rx)) where
367 fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x))
368 fip62 = cong₂ (λ j k → & (j , k )) *iso *iso
367 fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) )) 369 fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) ))
368 fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where 370 fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
369 fip34 : * z1 ⊆ L 371 fip34 : * z1 ⊆ L
370 fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1 372 fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1
371 fip33 : z1 ≡ & (L ＼ * x) 373 fip33 : z1 ≡ & (L ＼ * x)
380 fip62 = cong (&) ( begin 382 fip62 = cong (&) ( begin
381 (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ *iso *iso ⟩ 383 (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ *iso *iso ⟩
382 finCoverSet x sx ∪ finCoverSet y sy ∎ ) where open ≡-Reasoning 384 finCoverSet x sx ∪ finCoverSet y sy ∎ ) where open ≡-Reasoning
383 -- is also a cover 385 -- is also a cover
384 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L 386 isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
385 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L) ? where 387 isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L)
386 fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪ (L ＼ b)) 388 (fip70 o∅ (finCoverBase xo xcp)) where
387 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x) 389 fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x)
388 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫ 390 fip70 x (gi rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt }
389 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫ 391 fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers
390 fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) ) 392 (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} ? ? ) where
391 fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where 393 fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪ (L ＼ b))
392 fip44 : {x : Ordinal} → odef (L ＼ (a ∩ b)) x → Ordinal 394 fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x)
393 fip44 {x} Lab with fip45 {L} {a} {b} Lab 395 ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫
394 ... | case1 La = cover ca La 396 ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫
395 ... | case2 Lb = cover cb Lb 397 fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) )
396 fip46 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef A (fip44 lt) 398 fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where
397 fip46 {x} Lab with fip45 {L} {a} {b} Lab 399 fip44 : {x : Ordinal} → odef (L ＼ (a ∩ b)) x → Ordinal
398 ... | case1 La = P∋cover ca La 400 fip44 {x} Lab with fip45 {L} {a} {b} Lab
399 ... | case2 Lb = P∋cover cb Lb 401 ... | case1 La = cover ca La
400 fip47 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef (* (fip44 lt)) x 402 ... | case2 Lb = cover cb Lb
401 fip47 {x} Lab with fip45 {L} {a} {b} Lab 403 fip46 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef A (fip44 lt)
402 ... | case1 La = isCover ca La 404 fip46 {x} Lab with fip45 {L} {a} {b} Lab
403 ... | case2 Lb = isCover cb Lb 405 ... | case1 La = P∋cover ca La
404 fip40 : ( x y : Ordinal ) → * x ⊆ Replace (* X) (λ z → L ＼ z) → Subbase (* x) y 406 ... | case2 Lb = P∋cover cb Lb
405 → (Replace (* x) (λ z → L ＼ z )) covers (L ＼ * y ) 407 fip47 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef (* (fip44 lt)) x
406 fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace (* x) (λ z → L ＼ z)) covers ( L ＼ k ) ) (sym *iso) 408 fip47 {x} Lab with fip45 {L} {a} {b} Lab
407 ( fip43 {_} {L} {* a} {* b} fip41 fip42 ) where 409 ... | case1 La = isCover ca La
408 fip41 : Replace (* x) (λ z → L ＼ z) covers (L ＼ * a) 410 ... | case2 Lb = isCover cb Lb
409 fip41 = fip40 x a x⊆r sa
410 fip42 : Replace (* x) (λ z → L ＼ z) covers (L ＼ * b)
411 fip42 = fip40 x b x⊆r sb
412 fip40 x y x⊆r (gi sb) with x⊆r sb
413 ... | record { z = z ; az = az ; x=ψz = x=ψz } = record { cover = fip51 ; P∋cover = fip53 ; isCover = fip50 }where
414 fip51 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → Ordinal
415 fip51 {w} Lyw = z
416 fip52 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* X) z
417 fip52 {w} Lyw = az
418 fip55 : * z ⊆ L
419 fip55 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az)) wz1
420 fip56 : * z ≡ L ＼ * y
421 fip56 = begin
422 * z ≡⟨ sym (L＼Lx=x fip55 ) ⟩
423 L ＼ ( L ＼ * z ) ≡⟨ cong (λ k → L ＼ k) (sym *iso) ⟩
424 L ＼ * ( & ( L ＼ * z )) ≡⟨ cong (λ k → L ＼ * k) (sym x=ψz) ⟩
425 L ＼ * y ∎ where open ≡-Reasoning
426 fip53 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (Replace (* x) (λ z₁ → L ＼ z₁)) z
427 fip53 {w} Lyw = record { z = _ ; az = sb ; x=ψz = fip54 } where
428 fip54 : z ≡ & ( L ＼ * y )
429 fip54 = begin
430 z ≡⟨ sym &iso ⟩
431 & (* z) ≡⟨ cong (&) fip56 ⟩
432 & (L ＼ * y )
433 ∎ where open ≡-Reasoning
434 fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w
435 fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
436 411
437 open _==_ 412 open _==_
438 413
439 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top 414 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top
440 Compact→FIP {L} top compact with trio< (& L) o∅ 415 Compact→FIP {L} top compact with trio< (& L) o∅