Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1229:5e6dfe739f6a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Mar 2023 14:10:56 +0900 |
| parents | e3f20bc4fac9 |
| children | faffe9a4bd0f |
| files | src/Tychonoff.agda |
| diffstat | 1 files changed, 125 insertions(+), 86 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Wed Mar 08 10:28:55 2023 +0900 +++ b/src/Tychonoff.agda Wed Mar 08 14:10:56 2023 +0900 @@ -351,14 +351,17 @@ F⊆pxq : {x : HOD } → filter F ∋ x → x ⊆ ZFP P Q F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy) - isP→PxQ : {x : HOD} → (x⊆P : x ⊆ P ) → ZFP x Q ⊆ ZFP P Q + --- + --- FP is a P-projection of F, which is a ultra filter + --- + isP→PxQ : {x : HOD} → (x⊆P : x ⊆ P ) → ZFP x Q ⊆ ZFP P Q isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q - fx→px : {x : HOD } → filter F ∋ x → HOD + fx→px : {x : HOD } → filter F ∋ x → HOD fx→px {x} fx = Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )) fx→px1 : {p : HOD } {q : Ordinal } → odef Q q → (fp : filter F ∋ ZFP p Q ) → fx→px fp ≡ p fx→px1 {p} {q} qq fp = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where ty21 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >))) - ty21 pz qz = F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz )) + ty21 pz qz = F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz )) ty32 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → zπ1 (ty21 pz qz) ≡ a ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a @@ -366,45 +369,49 @@ ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c) ty20 : {x : Ordinal} → odef (fx→px fp) x → odef p x ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef p k) a=x pz where - ty24 : * x ≡ * a + ty24 : * x ≡ * a ty24 = begin * x ≡⟨ cong (*) x=ψz ⟩ _ ≡⟨ *iso ⟩ * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ cong (*) (ty32 pz qz) ⟩ * a ∎ where open ≡-Reasoning - a=x : a ≡ x + a=x : a ≡ x a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) - ty22 : {x : Ordinal} → odef p x → odef (fx→px fp) x + ty22 : {x : Ordinal} → odef p x → odef (fx→px fp) x ty22 {x} px = record { z = _ ; az = ab-pair px qq ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where ty12 : * x ≡ * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq )))) ty12 = begin * x ≡⟨ sym (cong (*) (ty32 px qq )) ⟩ * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq )))) ∎ where open ≡-Reasoning + + -- Projection of F FPSet : HOD FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) ))) + + -- Projection ⁻¹ F (which is in F) is in FPSet FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋ ZFP q Q → FPSet ∋ q FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where -- brain damaged one - ty11 : {y : HOD} {xy : (* (& (ZFP q Q))) ∋ y } → + ty11 : {y : HOD} {xy : (* (& (ZFP q Q))) ∋ y } → * (zπ1 ( (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ * (zπ1 ( (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) ty11 {y} {xy} = cong (λ k → * (zπ1 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy - b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) + b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ty10 : Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q ty10 = begin - Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) - ≡⟨ + Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) + ≡⟨ cong (λ k → Replace' (* (& (ZFP q Q))) k ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy})))) ⟩ - Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) + Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) ≡⟨ Replace'-iso _ ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ⟩ - Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ + Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ fx→px fq ≡⟨ fx→px1 aq fq ⟩ q ∎ where open ≡-Reasoning FPSet⊆PP : FPSet ⊆ Power P 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 - ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } - = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) + ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } + = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1)) ) X=F1 : (x : Ordinal) (p : HOD) (fx : odef (filter F) x) → Set n X=F1 x p fx = & p ≡ & (Replace' (* x) (λ y xy → @@ -415,22 +422,22 @@ x⊆pxq {x} {p} fx x=ψz {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where ty21 : ZFProduct P Q (& (* (& < * a , * b >))) - ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw) + ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw) ty32 : ZFProduct P Q (& (* (& < * a , * b >))) ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx) - (& (* (& < * a , * b >))) (subst (λ k → odef k + (& (* (& < * a , * b >))) (subst (λ k → odef k (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw)) - ty07 : odef (* x) (& < * a , * b >) + ty07 : odef (* x) (& < * a , * b >) ty07 = xw ty08 : odef p a - ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz))) + ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz))) record { z = _ ; az = xw ; x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c) p⊆P : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F1 x p fx → p ⊆ P 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 - ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) + ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) FP : Filter {Power P} {P} (λ x → x) FP = record { filter = FPSet ; f⊆L = FPSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where @@ -451,7 +458,7 @@ ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq ty02 : {p q : HOD} → FPSet ∋ p → FPSet ∋ q → Power P ∋ (p ∩ q) → FPSet ∋ (p ∩ q) ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } - record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq + record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq = FPSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q) ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where @@ -461,13 +468,13 @@ pqz1 = p⊆P fzp x=ψzp (proj1 (zp1 pqz)) pqz2 : odef Q (zπ2 pqz) pqz2 = zp2 pqz - ty53 : filter F ∋ ZFP p Q - ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp) - (subst (λ k → odef k z) *iso wz)) + ty53 : filter F ∋ ZFP p Q + ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp) + (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp) - ty52 : filter F ∋ ZFP q Q - ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq) - (subst (λ k → odef k z) *iso wz)) + ty52 : filter F ∋ ZFP q Q + ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq) + (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq) ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q ) ty51 = filter2 F ty53 ty52 ty54 @@ -476,33 +483,35 @@ UFP : ultra-filter FP UFP = record { proper = ty61 ; ultra = ty60 } where ty61 : ¬ (FPSet ∋ od∅) - ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where + ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where ty63 : {x : Ordinal} → ¬ odef (* z) x ty63 {x} zx with x⊆pxq az x=ψz zx ... | ab-pair xp xq = ¬x<0 xp ty62 : odef (filter F) (& od∅) ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az ty60 : {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (FPSet ∋ p) ∨ (FPSet ∋ (P ＼ p)) - ty60 {p} Pp Pnp with ultra-filter.ultra UF {ZFP p Q} - (λ z xz → isP→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) + ty60 {p} Pp Pnp with ultra-filter.ultra UF {ZFP p Q} + (λ z xz → isP→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) (λ z xz → proj1 (subst (λ k → odef k z) *iso xz )) ... | case1 fp = case1 (FPSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fp ) ... | case2 fnp = case2 (FPSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj1 ZFP\Q)) fnp )) uflp : UFLP TP FP UFP uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP + + -- FPSet is in Projection ⁻¹ F FPSet⊆F : {x : Ordinal } → odef FPSet x → odef (filter F) (& (ZFP (* x) Q)) FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = ? -- copy and pasted, sorry -- - isQ→PxQ : {x : HOD} → (x⊆Q : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q - isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) - fx→qx : {x : HOD } → filter F ∋ x → HOD + isQ→PxQ : {x : HOD} → (x⊆Q : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q + isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) + fx→qx : {x : HOD } → filter F ∋ x → HOD fx→qx {x} fx = Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) )) fx→qx1 : {q : HOD } {p : Ordinal } → odef P p → (fq : filter F ∋ ZFP P q ) → fx→qx fq ≡ q fx→qx1 {q} {p} qq fq = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where ty21 : {a b : Ordinal } → (qz : odef q b) → (pz : odef P a) → ZFProduct P Q (& (* (& < * a , * b >))) - ty21 qz pz = F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair pz qz )) + ty21 qz pz = F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair pz qz )) ty32 : {a b : Ordinal } → (qz : odef q b) → (pz : odef P a) → zπ2 (ty21 qz pz) ≡ b ty32 {a} {b} pz qz = ty33 (ty21 pz qz) (cong (&) *iso) where ty33 : {a b x : Ordinal } ( q : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 q ≡ b @@ -510,15 +519,15 @@ ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d) ty20 : {x : Ordinal} → odef (fx→qx fq) x → odef q x ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef q k) b=x qz where - ty24 : * x ≡ * b + ty24 : * x ≡ * b ty24 = begin * x ≡⟨ cong (*) x=ψz ⟩ _ ≡⟨ *iso ⟩ * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ cong (*) (ty32 qz pz) ⟩ * b ∎ where open ≡-Reasoning - b=x : b ≡ x + b=x : b ≡ x b=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) - ty22 : {x : Ordinal} → odef q x → odef (fx→qx fq) x + ty22 : {x : Ordinal} → odef q x → odef (fx→qx fq) x ty22 {x} qx = record { z = _ ; az = ab-pair qq qx ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) } where ty12 : * x ≡ * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx )))) ty12 = begin @@ -529,26 +538,26 @@ FQSet∋zpq : {q : HOD} → q ⊆ Q → filter F ∋ ZFP P q → FQSet ∋ q FQSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where -- brain damaged one - ty11 : {y : HOD} {xy : (* (& (ZFP P q ))) ∋ y } → + ty11 : {y : HOD} {xy : (* (& (ZFP P q ))) ∋ y } → * (zπ2 ( (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ * (zπ2 ( (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) ty11 {y} {xy} = cong (λ k → * (zπ2 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy - b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) + b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ty10 : Replace' (* (& (ZFP P q ))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q ty10 = begin - Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) - ≡⟨ + Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) + ≡⟨ cong (λ k → Replace' (* (& (ZFP P q ))) k ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy})))) ⟩ - Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) + Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy) ))) ≡⟨ Replace'-iso _ ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ⟩ - Replace' (ZFP P q ) ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ + Replace' (ZFP P q ) ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ fx→qx fq ≡⟨ fx→qx1 ap fq ⟩ q ∎ where open ≡-Reasoning FQSet⊆PP : FQSet ⊆ Power Q 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 - ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } - = subst (λ k → odef Q k) (sym (trans x=ψz1 &iso)) + ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } + = subst (λ k → odef Q k) (sym (trans x=ψz1 &iso)) (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1)) ) X=F2 : (x : Ordinal) (q : HOD) (fx : odef (filter F) x) → Set n X=F2 x q fx = & q ≡ & (Replace' (* x) (λ y xy → @@ -559,43 +568,43 @@ x⊆qxq {x} {p} fx x=ψz {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw ... | ab-pair {a} {b} pw qw = ab-pair pw ty08 where ty21 : ZFProduct P Q (& (* (& < * a , * b >))) - ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw) + ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw) ty32 : ZFProduct P Q (& (* (& < * a , * b >))) ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx) - (& (* (& < * a , * b >))) (subst (λ k → odef k + (& (* (& < * a , * b >))) (subst (λ k → odef k (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw)) - ty07 : odef (* x) (& < * a , * b >) + ty07 : odef (* x) (& < * a , * b >) ty07 = xw ty08 : odef p b - ty08 = subst (λ k → odef k b ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz))) + ty08 = subst (λ k → odef k b ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz))) record { z = _ ; az = xw ; x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d) q⊆Q : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F2 x p fx → p ⊆ Q 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 - ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef Q k) (sym (trans x=ψz1 &iso)) + ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef Q k) (sym (trans x=ψz1 &iso)) (zp2 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) FQ : Filter {Power Q} {Q} (λ x → x) FQ = record { filter = FQSet ; f⊆L = FQSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where ty01 : {p q : HOD} → Power Q ∋ q → FQSet ∋ p → p ⊆ q → FQSet ∋ q - ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FQSet∋zpq q⊆P (ty10 ty05 ty06 ) + ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FQSet∋zpq q⊆P (ty10 ty05 ty06 ) where -- p ≡ (Replace' (* x) (λ y xy → (zπ2 (F⊆qxq (subst (odef (filter F)) (sym &iso) fx) xy)) -- x = ( px , qx ) , qx ⊆ q - ty03 : Power (ZFP P Q) ∋ ZFP P q - ty03 z zpq = isQ→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP P k ) (sym *iso))) zpq ) + ty03 : Power (ZFP P Q) ∋ ZFP P q + ty03 z zpq = isQ→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP P k ) (sym *iso))) zpq ) q⊆P : q ⊆ Q q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) ty05 : filter F ∋ ZFP P p 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) - ty06 : ZFP P p ⊆ ZFP P q - ty06 (ab-pair wp wq ) = ab-pair wp (p⊆q wq) - ty10 : filter F ∋ ZFP P p → ZFP P p ⊆ ZFP P q → filter F ∋ ZFP P q + ty06 : ZFP P p ⊆ ZFP P q + ty06 (ab-pair wp wq ) = ab-pair wp (p⊆q wq) + ty10 : filter F ∋ ZFP P p → ZFP P p ⊆ ZFP P q → filter F ∋ ZFP P q ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq ty02 : {p q : HOD} → FQSet ∋ p → FQSet ∋ q → Power Q ∋ (p ∩ q) → FQSet ∋ (p ∩ q) ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } - record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq + record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq = FQSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where ty54 : Power (ZFP P Q) ∋ (ZFP P p ∩ ZFP P q ) ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where @@ -605,46 +614,51 @@ pqz1 = zp1 pqz pqz2 : odef Q (zπ2 pqz) pqz2 = q⊆Q fzp x=ψzp (proj1 (zp2 pqz)) - ty53 : filter F ∋ ZFP P p - ty53 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzp x=ψzp) - (subst (λ k → odef k z) *iso wz)) + ty53 : filter F ∋ ZFP P p + ty53 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzp x=ψzp) + (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆qxq fzp x=ψzp) - ty52 : filter F ∋ ZFP P q - ty52 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzq x=ψzq) - (subst (λ k → odef k z) *iso wz)) + ty52 : filter F ∋ ZFP P q + ty52 = filter1 F (λ z wz → isQ→PxQ (q⊆Q fzq x=ψzq) + (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆qxq fzq x=ψzq) ty51 : filter F ∋ ( ZFP P p ∩ ZFP P q ) ty51 = filter2 F ty53 ty52 ty54 - ty50 : filter F ∋ ZFP P (p ∩ q) + ty50 : filter F ∋ ZFP P (p ∩ q) ty50 = subst (λ k → filter F ∋ k ) (sym (proj2 ZFP∩)) ty51 UFQ : ultra-filter FQ UFQ = record { proper = ty61 ; ultra = ty60 } where ty61 : ¬ (FQSet ∋ od∅) - ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where + ty61 record { z = z ; az = az ; x=ψz = x=ψz } = ultra-filter.proper UF ty62 where ty63 : {x : Ordinal} → ¬ odef (* z) x ty63 {x} zx with x⊆qxq az x=ψz zx ... | ab-pair xp xq = ¬x<0 xq ty62 : odef (filter F) (& od∅) ty62 = subst (λ k → odef (filter F) k ) (trans (sym &iso) (cong (&) (¬x∋y→x≡od∅ ty63)) ) az ty60 : {p : HOD} → Power Q ∋ p → Power Q ∋ (Q ＼ p) → (FQSet ∋ p) ∨ (FQSet ∋ (Q ＼ p)) - ty60 {q} Pp Pnp with ultra-filter.ultra UF {ZFP P q} - (λ z xz → isQ→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) + ty60 {q} Pp Pnp with ultra-filter.ultra UF {ZFP P q} + (λ z xz → isQ→PxQ (λ {x} lt → Pp _ (subst (λ k → odef k x) (sym *iso) lt)) (subst (λ k → odef k z) *iso xz)) (λ z xz → proj1 (subst (λ k → odef k z) *iso xz )) ... | case1 fq = case1 (FQSet∋zpq (λ {z} xz → Pp z (subst (λ k → odef k z) (sym *iso) xz )) fq ) ... | case2 fnp = case2 (FQSet∋zpq (λ pp → proj1 pp) (subst (λ k → odef (filter F) k) (cong (&) (proj2 ZFP\Q)) fnp )) + + -- FQSet is in Projection ⁻¹ F + FQSet⊆F : {x : Ordinal } → odef FQSet x → odef (filter F) (& (ZFP P (* x) )) + FQSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = ? + uflq : UFLP TQ FQ UFQ uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) - Pf = ab-pair (UFLP.P∋limit uflp) (UFLP.P∋limit uflq) + Pf = ab-pair (UFLP.P∋limit uflp) (UFLP.P∋limit uflq) record aSubbase (b : Ordinal) : Set n where field - fp∋b∨fq∋b : odef (filter FP ) b ∨ odef (filter FP ) b - + fp∋b∨fq∋b : odef (filter FP ) b ∨ odef (filter FP ) b + isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v - isL {v} npq = filter1 F (λ z xz → Neighbor.v⊆P npq (subst (λ k → odef k z) *iso xz)) - (subst (λ k → odef (filter F) k) (sym &iso) (F∋base pqb npq pqb⊆opq)) bpq⊆v where + isL {v} nei = filter1 F (λ z xz → Neighbor.v⊆P nei (subst (λ k → odef k z) *iso xz)) + (subst (λ k → odef (filter F) k) (sym &iso) (F∋base pqb b∋l )) bpq⊆v where -- -- Product Topolgy's open set contains a subbase which is an element of ZPF p Q or ZPF P q -- Neighbor of limit contains an open set which conatins a limit @@ -652,33 +666,58 @@ -- so there is a subbase which contains a limit, the subbase is an element of projection of a filter (P or Q) TPQ = ProductTopology TP TQ lim = & < * (UFLP.limit uflp) , * (UFLP.limit uflq) > - bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) - bpq = Neighbor.ou npq (Neighbor.ux npq) + bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u nei) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) + bpq = Neighbor.ou nei (Neighbor.ux nei) + b∋l : odef (* (Base.b bpq)) lim + b∋l = Base.bx bpq pqb : Subbase (pbase TP TQ) (Base.b bpq ) pqb = Base.sb bpq - pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq ) + pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u nei ) bpq⊆v : * (Base.b bpq) ⊆ * v - bpq⊆v {x} bx = Neighbor.u⊆v npq (pqb⊆opq bx) + bpq⊆v {x} bx = Neighbor.u⊆v nei (pqb⊆opq bx) pqb⊆opq = Base.b⊆u bpq - F∋base : {b v : Ordinal } → Subbase (pbase TP TQ) b → (npq : Neighbor TPQ lim v) → * b ⊆ * (Neighbor.u npq) → odef (filter F) b - F∋base {b} {v} (gi (case1 px)) npq b⊆u = subst (λ k → odef (filter F) k) (sym (BaseP.prod px)) f∋b where + F∋base : {b : Ordinal } → Subbase (pbase TP TQ) b → odef (* b) lim → odef (filter F) b + F∋base {b} (gi (case1 px)) bl = subst (λ k → odef (filter F) k) (sym (BaseP.prod px)) f∋b where + -- + -- subbase of product topology which includes lim is in FP, so in F + -- + isl00 : odef (ZFP (* (BaseP.p px)) Q) lim + isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseP.prod px)) *iso ) bl px∋limit : odef (* (BaseP.p px)) (UFLP.limit uflp) - px∋limit = ? + px∋limit = isl01 isl00 refl where + isl01 : {x : Ordinal } → odef (ZFP (* (BaseP.p px)) Q) x → x ≡ lim → odef (* (BaseP.p px)) (UFLP.limit uflp) + isl01 (ab-pair {a} {b} bx qx) ab=lim = subst (λ k → odef (* (BaseP.p px)) k) a=lim bx where + a=lim : a ≡ UFLP.limit uflp + a=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) ))) fp∋b : filter FP ∋ * (BaseP.p px) - fp∋b = UFLP.is-limit uflp record { u = _ ; ou = BaseP.op px ; ux = px∋limit + fp∋b = UFLP.is-limit uflp record { u = _ ; ou = BaseP.op px ; ux = px∋limit ; v⊆P = λ {x} lt → os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) (BaseP.op px)) lt ; u⊆v = λ x → x } f∋b : odef (filter F) (& (ZFP (* (BaseP.p px)) Q)) f∋b = FPSet⊆F (subst (λ k → odef (filter FP) k ) &iso fp∋b ) - F∋base (gi (case2 qx)) npq b⊆u = ? - F∋base (g∩ {x} {y} b1 b2) npq xy⊆u = F∋x∩y where + F∋base {b} (gi (case2 qx)) bl = subst (λ k → odef (filter F) k) (sym (BaseQ.prod qx)) f∋b where + isl00 : odef (ZFP P (* (BaseQ.q qx))) lim + isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseQ.prod qx)) *iso ) bl + qx∋limit : odef (* (BaseQ.q qx)) (UFLP.limit uflq) + qx∋limit = isl01 isl00 refl where + isl01 : {x : Ordinal } → odef (ZFP P (* (BaseQ.q qx)) ) x → x ≡ lim → odef (* (BaseQ.q qx)) (UFLP.limit uflq) + isl01 (ab-pair {a} {b} px bx) ab=lim = subst (λ k → odef (* (BaseQ.q qx)) k) b=lim bx where + b=lim : b ≡ UFLP.limit uflq + b=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) ))) + fp∋b : filter FQ ∋ * (BaseQ.q qx) + fp∋b = UFLP.is-limit uflq record { u = _ ; ou = BaseQ.oq qx ; ux = qx∋limit + ; v⊆P = λ {x} lt → os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) (BaseQ.oq qx)) lt ; u⊆v = λ x → x } + f∋b : odef (filter F) (& (ZFP P (* (BaseQ.q qx)) )) + f∋b = FQSet⊆F (subst (λ k → odef (filter FQ) k ) &iso fp∋b ) + F∋base (g∩ {x} {y} b1 b2) bl = F∋x∩y where + -- filter contains finite intersection fb01 : odef (filter F) x - fb01 = F∋base b1 ? ? + fb01 = F∋base b1 (proj1 (subst (λ k → odef k lim) *iso bl)) fb02 : odef (filter F) y - fb02 = F∋base b2 ? ? + fb02 = F∋base b2 (proj2 (subst (λ k → odef k lim) *iso bl)) F∋x∩y : odef (filter F) (& (* x ∩ * y)) - F∋x∩y = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) fb01) (subst (λ k → odef (filter F) k) (sym &iso) fb02) - (CAP (ZFP P Q) (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb01)) - (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb02))) + F∋x∩y = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) fb01) (subst (λ k → odef (filter F) k) (sym &iso) fb02) + (CAP (ZFP P Q) (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb01)) + (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb02)))