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

comparison src/Tychonoff.agda @ 1298:2c34f2b554cf current

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replace and filter projection fix done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 03 Jun 2023 17:31:17 +0900
parents 968feed7cf64
children 47d3cc596d68
comparison
equal deleted inserted replaced
1297:ad9ed7c4a0b3 1298:2c34f2b554cf
30 30
31 import ODC 31 import ODC
32 open ODC O 32 open ODC O
33 33
34 open import filter O 34 open import filter O
35 open import filter-util O
35 open import ZProduct O 36 open import ZProduct O
36 open import Topology O 37 open import Topology O
37 -- open import maximum-filter O 38 -- open import maximum-filter O
38 39
39 open Filter 40 open Filter
419 F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy) 420 F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy)
420 421
421 --- 422 ---
422 --- FP is a P-projection of F, which is a ultra filter 423 --- FP is a P-projection of F, which is a ultra filter
423 --- 424 ---
424 isP→PxQ : {x : HOD} → (x⊆P : x ⊆ P ) → ZFP x Q ⊆ ZFP P Q
425 isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q
426 fx→px : {x : HOD } → filter F ∋ x → HOD
427 fx→px {x} fx = Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )) {P} record { ≤COD = λ {x} lt {y} ly → ? }
428 fx→px1 : {p : HOD } {q : Ordinal } → odef Q q → (fp : filter F ∋ ZFP p Q ) → fx→px fp ≡ p
429 fx→px1 {p} {q} qq fp = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where
430 ty21 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >)))
431 ty21 pz qz = F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz ))
432 ty32 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → zπ1 (ty21 pz qz) ≡ a
433 ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where
434 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
435 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
436 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c)
437 ty20 : {x : Ordinal} → odef (fx→px fp) x → odef p x
438 ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef p k) a=x pz where
439 ty24 : * x ≡ * a
440 ty24 = begin
441 * x ≡⟨ cong (*) x=ψz ⟩
442 _ ≡⟨ *iso ⟩
443 * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ cong (*) (ty32 pz qz) ⟩
444 * a ∎ where open ≡-Reasoning
445 a=x : a ≡ x
446 a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24))
447 ty22 : {x : Ordinal} → odef p x → odef (fx→px fp) x
448 ty22 {x} px = record { z = _ ; az = ab-pair px qq ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where
449 ty12 : * x ≡ * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq ))))
450 ty12 = begin
451 * x ≡⟨ sym (cong (*) (ty32 px qq )) ⟩
452 * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq )))) ∎ where open ≡-Reasoning
453
454 -- Projection of F
455 FPSet : HOD
456 FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )) ? ) ?
457
458 -- Projection ⁻¹ F (which is in F) is in FPSet
459 FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋ ZFP q Q → FPSet ∋ q
460 FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where
461 -- brain damaged one
462 ty11 : {y : HOD} {xy : (* (& (ZFP q Q))) ∋ y } →
463 * (zπ1 ( (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ * (zπ1 ( (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) )))
464 ty11 {y} {xy} = cong (λ k → * (zπ1 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where
465 a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy
466 b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)
467 ty10 : Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ? ≡ q
468 ty10 = begin
469 Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ?
470 ≡⟨
471 cong (λ k → Replace' (* (& (ZFP q Q))) k ? ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy}))))
472 ⟩
473 Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) ?
474 ≡⟨ Replace'-iso _ ? ? ? ⟩
475 Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ? ≡⟨ refl ⟩
476 fx→px fq ≡⟨ fx→px1 aq fq ⟩
477 q ∎ where open ≡-Reasoning
478 FPSet⊆PP : FPSet ⊆ Power P
479 FPSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw
480 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 }
481 = subst (λ k → odef P k) (sym (trans x=ψz1 &iso))
482 (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1)) )
483 X=F1 : (x : Ordinal) (p : HOD) (fx : odef (filter F) x) → Set n
484 X=F1 x p fx = & p ≡ & (Replace' (* x) (λ y xy →
485 * (zπ1 (f⊆L F
486 (subst (odef (filter F)) (sym &iso) fx)
487 (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy)))) ? )
488 x⊆pxq : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F1 x p fx → * x ⊆ ZFP p Q
489 x⊆pxq {x} {p} fx x=ψz {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
490 ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where
491 ty21 : ZFProduct P Q (& (* (& < * a , * b >)))
492 ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw)
493 ty32 : ZFProduct P Q (& (* (& < * a , * b >)))
494 ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx)
495 (& (* (& < * a , * b >))) (subst (λ k → odef k
496 (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw))
497 ty07 : odef (* x) (& < * a , * b >)
498 ty07 = xw
499 ty08 : odef p a
500 ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz)))
501 record { z = _ ; az = xw ; x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where
502 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
503 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
504 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c)
505 p⊆P : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F1 x p fx → p ⊆ P
506 p⊆P {x} {p} fx x=ψz {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz)) pw
507 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso))
508 (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) )
509 FP : Filter {Power P} {P} (λ x → x) 425 FP : Filter {Power P} {P} (λ x → x)
510 FP = record { filter = FPSet ; f⊆L = FPSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where 426 FP = Filter-Proj1 {P} {Q} is-apq F
511 ty01 : {p q : HOD} → Power P ∋ q → FPSet ∋ p → p ⊆ q → FPSet ∋ q
512 ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FPSet∋zpq q⊆P (ty10 ty05 ty06 )
513 where
514 -- p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fx) xy))
515 -- x = ( px , qx ) , px ⊆ q
516 ty03 : Power (ZFP P Q) ∋ ZFP q Q
517 ty03 z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq )
518 q⊆P : q ⊆ P
519 q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw )
520 ty05 : filter F ∋ ZFP p Q
521 ty05 = filter1 F (λ z wz → isP→PxQ (p⊆P fx x=ψz) (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) (x⊆pxq fx x=ψz)
522 ty06 : ZFP p Q ⊆ ZFP q Q
523 ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq
524 ty10 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q
525 ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq
526 ty02 : {p q : HOD} → FPSet ∋ p → FPSet ∋ q → Power P ∋ (p ∩ q) → FPSet ∋ (p ∩ q)
527 ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp }
528 record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq
529 = FPSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where
530 ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q)
531 ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where
532 pqz : odef (ZFP (p ∩ q) Q) z
533 pqz = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) )) xz
534 pqz1 : odef P (zπ1 pqz)
535 pqz1 = p⊆P fzp x=ψzp (proj1 (zp1 pqz))
536 pqz2 : odef Q (zπ2 pqz)
537 pqz2 = zp2 pqz
538 ty53 : filter F ∋ ZFP p Q
539 ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp)
540 (subst (λ k → odef k z) *iso wz))
541 (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp)
542 ty52 : filter F ∋ ZFP q Q
543 ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq)
544 (subst (λ k → odef k z) *iso wz))
545 (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq)
546 ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q )
547 ty51 = filter2 F ty53 ty52 ty54
548 ty50 : filter F ∋ ZFP (p ∩ q) Q
549 ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51
550 UFP : ultra-filter FP 427 UFP : ultra-filter FP
551 UFP = record { proper = ty61 ; ultra = ty60 } where 428 UFP = Filter-Proj1-UF {P} {Q} is-apq F UF
552 ty61 : ¬ (FPSet ∋ od∅)
553 ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where
554 ty63 : {x : Ordinal} → ¬ odef (* z) x
555 ty63 {x} zx with x⊆pxq az x=ψz zx
556 ... | ab-pair xp xq = ¬x<0 xp
557 ty62 : odef (filter F) (& od∅)
558 ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az
559 ty60 : {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (FPSet ∋ p) ∨ (FPSet ∋ (P ＼ p))
560 ty60 {p} Pp Pnp with ultra-filter.ultra UF {ZFP p Q}
561 (λ z xz → isP→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz))
562 (λ z xz → proj1 (subst (λ k → odef k z) *iso xz ))
563 ... | case1 fp = case1 (FPSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fp )
564 ... | case2 fnp = case2 (FPSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj1 ZFP\Q)) fnp ))
565 uflp : UFLP TP FP UFP 429 uflp : UFLP TP FP UFP
566 uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP 430 uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
567 431
568 -- FPSet is in Projection ⁻¹ F 432 -- FPSet is in Projection ⁻¹ F
569 FPSet⊆F : {x : Ordinal } → odef FPSet x → odef (filter F) (& (ZFP (* x) Q)) 433 FPSet⊆F1 : {x : Ordinal } → odef (filter FP) x → odef (filter F) (& (ZFP (* x) Q))
570 FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F ty80 (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where 434 FPSet⊆F1 {x} fpx = FPSet⊆F is-apq F fpx
571 Rx : HOD 435
572 Rx = Replace' (* z) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy))) ?
573 RxQ∋z : * z ⊆ ZFP Rx Q
574 RxQ∋z {w} zw = subst (λ k → ZFProduct Rx Q k ) ty70 ( ab-pair record { z = w ; az = zw ; x=ψz = refl } (zp2 b )) where
575 a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)
576 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw )
577 ty73 : & (* (zπ1 a)) ≡ zπ1 b
578 ty73 = begin
579 & (* (zπ1 a)) ≡⟨ &iso ⟩
580 zπ1 a ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩
581 zπ1 b ∎ where open ≡-Reasoning
582 ty70 : & < * (& (* (zπ1 a))) , * (zπ2 b) > ≡ w
583 ty70 with zp-iso (subst (λ k → odef (ZFP P Q) k) (sym &iso) (f⊆L F az _ zw ))
584 ... | eq = trans (cong₂ (λ j k → & < * j , k > ) ty73 refl ) (trans eq &iso )
585 ty71 : * z ⊆ ZFP (* x) Q
586 ty71 = subst (λ k → * z ⊆ ZFP k Q) ty72 RxQ∋z where
587 ty72 : Rx ≡ * x
588 ty72 = begin
589 Rx ≡⟨ sym *iso ⟩
590 * (& Rx) ≡⟨ cong (*) (sym x=ψz ) ⟩
591 * x ∎ where open ≡-Reasoning
592 ty80 : Power (ZFP P Q) ∋ ZFP (* x) Q
593 ty80 y yx = isP→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where
594 ty81 : * x ⊆ P
595 ty81 {w} xw with subst (λ k → odef k w) (trans (cong (*) x=ψz ) *iso ) xw
596 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym ty84) ty87 where
597 a = f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1))
598 (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1))
599 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) (f⊆L F az _ az1 )
600 ty87 : odef P (zπ1 b)
601 ty87 = zp1 b
602 ty84 : w ≡ (zπ1 b)
603 ty84 = begin
604 w ≡⟨ trans x=ψz1 &iso ⟩
605 zπ1 a ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b )) ⟩
606 zπ1 b ∎ where open ≡-Reasoning
607
608 -- copy and pasted, sorry
609 --
610 isQ→PxQ : {x : HOD} → (x⊆Q : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q
611 isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q)
612 fx→qx : {x : HOD } → filter F ∋ x → HOD
613 fx→qx {x} fx = Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) )) ?
614 fx→qx1 : {q : HOD } {p : Ordinal } → odef P p → (fq : filter F ∋ ZFP P q ) → fx→qx fq ≡ q
615 fx→qx1 {q} {p} qq fq = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where
616 ty21 : {a b : Ordinal } → (qz : odef q b) → (pz : odef P a) → ZFProduct P Q (& (* (& < * a , * b >)))
617 ty21 qz pz = F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair pz qz ))
618 ty32 : {a b : Ordinal } → (qz : odef q b) → (pz : odef P a) → zπ2 (ty21 qz pz) ≡ b
619 ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where
620 ty33 : {a b x : Ordinal } ( q : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 q ≡ b
621 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
622 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d)
623 ty20 : {x : Ordinal} → odef (fx→qx fq) x → odef q x
624 ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef q k) b=x qz where
625 ty24 : * x ≡ * b
626 ty24 = begin
627 * x ≡⟨ cong (*) x=ψz ⟩
628 _ ≡⟨ *iso ⟩
629 * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ cong (*) (ty32 qz pz) ⟩
630 * b ∎ where open ≡-Reasoning
631 b=x : b ≡ x
632 b=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24))
633 ty22 : {x : Ordinal} → odef q x → odef (fx→qx fq) x
634 ty22 {x} qx = record { z = _ ; az = ab-pair qq qx ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where
635 ty12 : * x ≡ * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx ))))
636 ty12 = begin
637 * x ≡⟨ sym (cong (*) (ty32 qx qq )) ⟩
638 * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx )))) ∎ where open ≡-Reasoning
639 FQSet : HOD
640 FQSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) )) ? ) ?
641 FQSet∋zpq : {q : HOD} → q ⊆ Q → filter F ∋ ZFP P q → FQSet ∋ q
642 FQSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where
643 -- brain damaged one
644 ty11 : {y : HOD} {xy : (* (& (ZFP P q ))) ∋ y } →
645 * (zπ2 ( (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ * (zπ2 ( (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) )))
646 ty11 {y} {xy} = cong (λ k → * (zπ2 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where
647 a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy
648 b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)
649 ty10 : Replace' (* (& (ZFP P q ))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ? ≡ q
650 ty10 = begin
651 Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ?
652 ≡⟨ Replace'-iso _ ? ? ? ⟩
653 Replace' (ZFP P q ) ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ? ≡⟨ refl ⟩
654 fx→qx fq ≡⟨ fx→qx1 ap fq ⟩
655 q ∎ where open ≡-Reasoning
656 FQSet⊆PP : FQSet ⊆ Power Q
657 FQSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw
658 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 }
659 = subst (λ k → odef Q k) (sym (trans x=ψz1 &iso))
660 (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1)) )
661 X=F2 : (x : Ordinal) (q : HOD) (fx : odef (filter F) x) → Set n
662 X=F2 x q fx = & q ≡ & (Replace' (* x) (λ y xy →
663 * (zπ2 (f⊆L F
664 (subst (odef (filter F)) (sym &iso) fx)
665 (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy)))) ? )
666 x⊆qxq : {x : Ordinal} {q : HOD} (fx : odef (filter F) x) → X=F2 x q fx → * x ⊆ ZFP P q
667 x⊆qxq {x} {p} fx x=ψz {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
668 ... | ab-pair {a} {b} pw qw = ab-pair pw ty08 where
669 ty21 : ZFProduct P Q (& (* (& < * a , * b >)))
670 ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw)
671 ty32 : ZFProduct P Q (& (* (& < * a , * b >)))
672 ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx)
673 (& (* (& < * a , * b >))) (subst (λ k → odef k
674 (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw))
675 ty07 : odef (* x) (& < * a , * b >)
676 ty07 = xw
677 ty08 : odef p b
678 ty08 = subst (λ k → odef k b ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz)))
679 record { z = _ ; az = xw ; x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where
680 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b
681 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
682 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d)
683 q⊆Q : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F2 x p fx → p ⊆ Q
684 q⊆Q {x} {p} fx x=ψz {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz)) pw
685 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef Q k) (sym (trans x=ψz1 &iso))
686 (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) )
687 FQ : Filter {Power Q} {Q} (λ x → x) 436 FQ : Filter {Power Q} {Q} (λ x → x)
688 FQ = record { filter = FQSet ; f⊆L = FQSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where 437 FQ = Filter-Proj2 {P} {Q} is-apq F
689 ty01 : {p q : HOD} → Power Q ∋ q → FQSet ∋ p → p ⊆ q → FQSet ∋ q
690 ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FQSet∋zpq q⊆P (ty10 ty05 ty06 )
691 where
692 -- p ≡ (Replace' (* x) (λ y xy → (zπ2 (F⊆qxq (subst (odef (filter F)) (sym &iso) fx) xy))
693 -- x = ( px , qx ) , qx ⊆ q
694 ty03 : Power (ZFP P Q) ∋ ZFP P q
695 ty03 z zpq = isQ→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP P k ) (sym *iso))) zpq )
696 q⊆P : q ⊆ Q
697 q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw )
698 ty05 : filter F ∋ ZFP P p
699 ty05 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fx x=ψz) (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) (x⊆qxq fx x=ψz)
700 ty06 : ZFP P p ⊆ ZFP P q
701 ty06 (ab-pair wp wq ) = ab-pair wp (p⊆q wq)
702 ty10 : filter F ∋ ZFP P p → ZFP P p ⊆ ZFP P q → filter F ∋ ZFP P q
703 ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq
704 ty02 : {p q : HOD} → FQSet ∋ p → FQSet ∋ q → Power Q ∋ (p ∩ q) → FQSet ∋ (p ∩ q)
705 ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp }
706 record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq
707 = FQSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where
708 ty54 : Power (ZFP P Q) ∋ (ZFP P p ∩ ZFP P q )
709 ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where
710 pqz : odef (ZFP P (p ∩ q) ) z
711 pqz = subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) )) xz
712 pqz1 : odef P (zπ1 pqz)
713 pqz1 = zp1 pqz
714 pqz2 : odef Q (zπ2 pqz)
715 pqz2 = q⊆Q fzp x=ψzp (proj1 (zp2 pqz))
716 ty53 : filter F ∋ ZFP P p
717 ty53 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzp x=ψzp)
718 (subst (λ k → odef k z) *iso wz))
719 (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆qxq fzp x=ψzp)
720 ty52 : filter F ∋ ZFP P q
721 ty52 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzq x=ψzq)
722 (subst (λ k → odef k z) *iso wz))
723 (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆qxq fzq x=ψzq)
724 ty51 : filter F ∋ ( ZFP P p ∩ ZFP P q )
725 ty51 = filter2 F ty53 ty52 ty54
726 ty50 : filter F ∋ ZFP P (p ∩ q)
727 ty50 = subst (λ k → filter F ∋ k ) (sym (proj2 ZFP∩)) ty51
728 UFQ : ultra-filter FQ 438 UFQ : ultra-filter FQ
729 UFQ = record { proper = ty61 ; ultra = ty60 } where 439 UFQ = Filter-Proj2-UF {P} {Q} is-apq F UF
730 ty61 : ¬ (FQSet ∋ od∅)
731 ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where
732 ty63 : {x : Ordinal} → ¬ odef (* z) x
733 ty63 {x} zx with x⊆qxq az x=ψz zx
734 ... | ab-pair xp xq = ¬x<0 xq
735 ty62 : odef (filter F) (& od∅)
736 ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az
737 ty60 : {p : HOD} → Power Q ∋ p → Power Q ∋ (Q ＼ p) → (FQSet ∋ p) ∨ (FQSet ∋ (Q ＼ p))
738 ty60 {q} Pp Pnp with ultra-filter.ultra UF {ZFP P q}
739 (λ z xz → isQ→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz))
740 (λ z xz → proj1 (subst (λ k → odef k z) *iso xz ))
741 ... | case1 fq = case1 (FQSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fq )
742 ... | case2 fnp = case2 (FQSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj2 ZFP\Q)) fnp ))
743
744 440
745 -- FQSet is in Projection ⁻¹ F 441 -- FQSet is in Projection ⁻¹ F
746 FQSet⊆F : {x : Ordinal } → odef FQSet x → odef (filter F) (& (ZFP P (* x) )) 442 FQSet⊆F1 : {x : Ordinal } → odef (filter FQ) x → odef (filter F) (& (ZFP P (* x) ))
747 FQSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F ty80 (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where 443 FQSet⊆F1 {x} fpx = FQSet⊆F is-apq F fpx
748 Rx : HOD
749 Rx = Replace' (* z) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy))) ?
750 PxRx∋z : * z ⊆ ZFP P Rx
751 PxRx∋z {w} zw = subst (λ k → ZFProduct P Rx k ) ty70 ( ab-pair (zp1 b) record { z = w ; az = zw ; x=ψz = refl } ) where
752 a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)
753 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw )
754 ty73 : & (* (zπ2 a)) ≡ zπ2 b
755 ty73 = begin
756 & (* (zπ2 a)) ≡⟨ &iso ⟩
757 zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩
758 zπ2 b ∎ where open ≡-Reasoning
759 ty70 : & < * (zπ1 b) , * (& (* (zπ2 a))) > ≡ w
760 ty70 with zp-iso (subst (λ k → odef (ZFP P Q) k) (sym &iso) (f⊆L F az _ zw ))
761 ... | eq = trans (cong₂ (λ j k → & < j , * k > ) refl ty73 ) (trans eq &iso )
762 ty71 : * z ⊆ ZFP P (* x)
763 ty71 = subst (λ k → * z ⊆ ZFP P k ) ty72 PxRx∋z where
764 ty72 : Rx ≡ * x
765 ty72 = begin
766 Rx ≡⟨ sym *iso ⟩
767 * (& Rx) ≡⟨ cong (*) (sym x=ψz ) ⟩
768 * x ∎ where open ≡-Reasoning
769 ty80 : Power (ZFP P Q) ∋ ZFP P (* x)
770 ty80 y yx = isQ→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where
771 ty81 : * x ⊆ Q
772 ty81 {w} xw with subst (λ k → odef k w) (trans (cong (*) x=ψz ) *iso ) xw
773 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef Q k) (sym ty84) ty87 where
774 a = f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1))
775 (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1))
776 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) (f⊆L F az _ az1 )
777 ty87 : odef Q (zπ2 b)
778 ty87 = zp2 b
779 ty84 : w ≡ (zπ2 b)
780 ty84 = begin
781 w ≡⟨ trans x=ψz1 &iso ⟩
782 zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b )) ⟩
783 zπ2 b ∎ where open ≡-Reasoning
784
785 444
786 uflq : UFLP TQ FQ UFQ 445 uflq : UFLP TQ FQ UFQ
787 uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ 446 uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ
788 447
789 Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) 448 Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
824 a=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) ))) 483 a=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) )))
825 fp∋b : filter FP ∋ * (BaseP.p px) 484 fp∋b : filter FP ∋ * (BaseP.p px)
826 fp∋b = UFLP.is-limit uflp record { u = _ ; ou = BaseP.op px ; ux = px∋limit 485 fp∋b = UFLP.is-limit uflp record { u = _ ; ou = BaseP.op px ; ux = px∋limit
827 ; v⊆P = λ {x} lt → os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) (BaseP.op px)) lt ; u⊆v = λ x → x } 486 ; v⊆P = λ {x} lt → os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) (BaseP.op px)) lt ; u⊆v = λ x → x }
828 f∋b : odef (filter F) (& (ZFP (* (BaseP.p px)) Q)) 487 f∋b : odef (filter F) (& (ZFP (* (BaseP.p px)) Q))
829 f∋b = FPSet⊆F (subst (λ k → odef (filter FP) k ) &iso fp∋b ) 488 f∋b = FPSet⊆F1 (subst (λ k → odef (filter FP) k ) &iso fp∋b )
830 F∋base {b} (gi (case2 qx)) bl = subst (λ k → odef (filter F) k) (sym (BaseQ.prod qx)) f∋b where 489 F∋base {b} (gi (case2 qx)) bl = subst (λ k → odef (filter F) k) (sym (BaseQ.prod qx)) f∋b where
831 isl00 : odef (ZFP P (* (BaseQ.q qx))) lim 490 isl00 : odef (ZFP P (* (BaseQ.q qx))) lim
832 isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseQ.prod qx)) *iso ) bl 491 isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseQ.prod qx)) *iso ) bl
833 qx∋limit : odef (* (BaseQ.q qx)) (UFLP.limit uflq) 492 qx∋limit : odef (* (BaseQ.q qx)) (UFLP.limit uflq)
834 qx∋limit = isl01 isl00 refl where 493 qx∋limit = isl01 isl00 refl where
838 b=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) ))) 497 b=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) )))
839 fp∋b : filter FQ ∋ * (BaseQ.q qx) 498 fp∋b : filter FQ ∋ * (BaseQ.q qx)
840 fp∋b = UFLP.is-limit uflq record { u = _ ; ou = BaseQ.oq qx ; ux = qx∋limit 499 fp∋b = UFLP.is-limit uflq record { u = _ ; ou = BaseQ.oq qx ; ux = qx∋limit
841 ; v⊆P = λ {x} lt → os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) (BaseQ.oq qx)) lt ; u⊆v = λ x → x } 500 ; v⊆P = λ {x} lt → os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) (BaseQ.oq qx)) lt ; u⊆v = λ x → x }
842 f∋b : odef (filter F) (& (ZFP P (* (BaseQ.q qx)) )) 501 f∋b : odef (filter F) (& (ZFP P (* (BaseQ.q qx)) ))
843 f∋b = FQSet⊆F (subst (λ k → odef (filter FQ) k ) &iso fp∋b ) 502 f∋b = FQSet⊆F1 (subst (λ k → odef (filter FQ) k ) &iso fp∋b )
844 F∋base (g∩ {x} {y} b1 b2) bl = F∋x∩y where 503 F∋base (g∩ {x} {y} b1 b2) bl = F∋x∩y where
845 -- filter contains finite intersection 504 -- filter contains finite intersection
846 fb01 : odef (filter F) x 505 fb01 : odef (filter F) x
847 fb01 = F∋base b1 (proj1 (subst (λ k → odef k lim) *iso bl)) 506 fb01 = F∋base b1 (proj1 (subst (λ k → odef k lim) *iso bl))
848 fb02 : odef (filter F) y 507 fb02 : odef (filter F) y