# HG changeset patch # User kono # Date 1678147203 -32400 # Node ID 9f955d49e162885bda260107d099b76c7c9d2254 # Parent 0e8306b146f6de1d801813419b7c3b9093bb0a01 Proj P of Filter F done diff -r 0e8306b146f6 -r 9f955d49e162 src/Tychonoff.agda --- a/src/Tychonoff.agda Mon Mar 06 20:13:00 2023 +0900 +++ b/src/Tychonoff.agda Tue Mar 07 09:00:03 2023 +0900 @@ -407,67 +407,74 @@ ... | 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=F : (x : Ordinal) (p : HOD) (fx : odef (filter F) x) → Set n + X=F x p fx = & p ≡ & (Replace' (* x) (λ y xy → + * (zπ1 (f⊆L F + (subst (odef (filter F)) (sym &iso) fx) + (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy))))) + x⊆pxq : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F x p fx → * x ⊆ ZFP p Q + 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) + 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 >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw)) + 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))) + 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=F 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)) + (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 ty01 : {p q : HOD} → Power P ∋ q → FPSet ∋ p → p ⊆ q → FPSet ∋ q ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FPSet∋zpq q⊆P (ty10 ty05 ty06 ) where - -- p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆pxq (subst (odef (filter.Filter.filter F)) (sym &iso) fx) xy)) + -- p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fx) xy)) -- x = ( px , qx ) , px ⊆ q ty03 : Power (ZFP P Q) ∋ ZFP q Q ty03 z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq ) - p⊆P : p ⊆ P - p⊆P {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)) - (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 )) ) q⊆P : q ⊆ P q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) - x⊆pxq : * x ⊆ ZFP p Q - x⊆pxq {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) - 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 >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw)) - 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))) - 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) ty05 : filter F ∋ ZFP p Q - ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) x⊆pxq + 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) ty06 : ZFP p Q ⊆ ZFP q Q ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq ty10 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q 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 = azp ; x=ψz = x=ψzp } record { z = zq ; az = azq ; x=ψz = x=ψzq } Ppq + ty02 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } + 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 - x⊆pxq : * ? ⊆ ZFP p Q - x⊆pxq = ? 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 pqz : odef (ZFP (p ∩ q) Q) z pqz = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) )) xz - pqz1 : odef P (zπ1 pqz) - pqz1 = ? - pqz2 : odef Q (zπ2 pqz) - pqz2 = ? + pqz1 : odef P (zπ1 pqz) + 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 ? (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) ? ) x⊆pxq + 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 = ? + 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 ty50 : filter F ∋ ZFP (p ∩ q) Q ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51 - UFP : ultra-filter FP UFP = record { proper = {!!} ; ultra = {!!} } uflp : UFLP TP FP UFP