Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1298:2c34f2b554cf current
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 | ad9ed7c4a0b3 |
| children | 054c2b0925c4 |
| files | src/Tychonoff.agda src/Tychonoff1.agda src/ZProduct.agda src/filter-util.agda src/ordinal.agda |
| diffstat | 5 files changed, 486 insertions(+), 549 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Sat Jun 03 08:13:50 2023 +0900 +++ b/src/Tychonoff.agda Sat Jun 03 17:31:17 2023 +0900 @@ -32,6 +32,7 @@ open ODC O open import filter O +open import filter-util O open import ZProduct O open import Topology O -- open import maximum-filter O @@ -421,367 +422,25 @@ --- --- 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} fx = Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )) {P} record { ≤COD = λ {x} lt {y} ly → ? } - 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 )) - 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 - 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) - 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 = 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 = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) - 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 } → - * (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) - 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))) ? - ≡⟨ - 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'-iso _ ? ? ? ⟩ - 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)) - (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 → - * (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=F1 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=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)) - (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 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 ) - q⊆P : q ⊆ P - q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) - ty05 : filter F ∋ ZFP p Q - 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 = 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 - 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 = 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)) - (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)) - (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 + FP = Filter-Proj1 {P} {Q} is-apq F 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 - 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)) - (λ 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 )) + UFP = Filter-Proj1-UF {P} {Q} is-apq F UF 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 } = filter1 F ty80 (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where - Rx : HOD - Rx = Replace' (* z) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy))) ? - RxQ∋z : * z ⊆ ZFP Rx Q - RxQ∋z {w} zw = subst (λ k → ZFProduct Rx Q k ) ty70 ( ab-pair record { z = w ; az = zw ; x=ψz = refl } (zp2 b )) where - a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw) - b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw ) - ty73 : & (* (zπ1 a)) ≡ zπ1 b - ty73 = begin - & (* (zπ1 a)) ≡⟨ &iso ⟩ - zπ1 a ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ - zπ1 b ∎ where open ≡-Reasoning - ty70 : & < * (& (* (zπ1 a))) , * (zπ2 b) > ≡ w - ty70 with zp-iso (subst (λ k → odef (ZFP P Q) k) (sym &iso) (f⊆L F az _ zw )) - ... | eq = trans (cong₂ (λ j k → & < * j , k > ) ty73 refl ) (trans eq &iso ) - ty71 : * z ⊆ ZFP (* x) Q - ty71 = subst (λ k → * z ⊆ ZFP k Q) ty72 RxQ∋z where - ty72 : Rx ≡ * x - ty72 = begin - Rx ≡⟨ sym *iso ⟩ - * (& Rx) ≡⟨ cong (*) (sym x=ψz ) ⟩ - * x ∎ where open ≡-Reasoning - ty80 : Power (ZFP P Q) ∋ ZFP (* x) Q - ty80 y yx = isP→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where - ty81 : * x ⊆ P - ty81 {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 ty84) ty87 where - a = f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1)) - (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1)) - b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) (f⊆L F az _ az1 ) - ty87 : odef P (zπ1 b) - ty87 = zp1 b - ty84 : w ≡ (zπ1 b) - ty84 = begin - w ≡⟨ trans x=ψz1 &iso ⟩ - zπ1 a ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b )) ⟩ - zπ1 b ∎ where open ≡-Reasoning + FPSet⊆F1 : {x : Ordinal } → odef (filter FP) x → odef (filter F) (& (ZFP (* x) Q)) + FPSet⊆F1 {x} fpx = FPSet⊆F is-apq F fpx - -- 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 - 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 )) - 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 - 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) - 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 = 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 = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24)) - 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 - * x ≡⟨ sym (cong (*) (ty32 qx qq )) ⟩ - * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx )))) ∎ where open ≡-Reasoning - FQSet : HOD - FQSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) )) ? ) ? - 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 } → - * (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) - 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'-iso _ ? ? ? ⟩ - 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)) - (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 → - * (zπ2 (f⊆L F - (subst (odef (filter F)) (sym &iso) fx) - (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy)))) ? ) - x⊆qxq : {x : Ordinal} {q : HOD} (fx : odef (filter F) x) → X=F2 x q fx → * x ⊆ ZFP P q - 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) - 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 b - 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)) - (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 ) - 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 ) - 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 - 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 - = 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 - pqz : odef (ZFP P (p ∩ q) ) z - pqz = subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) )) xz - pqz1 : odef P (zπ1 pqz) - 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)) - (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)) - (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 = subst (λ k → filter F ∋ k ) (sym (proj2 ZFP∩)) ty51 + FQ = Filter-Proj2 {P} {Q} is-apq F 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 - 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)) - (λ 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 )) - + UFQ = Filter-Proj2-UF {P} {Q} is-apq F UF -- 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 } = filter1 F ty80 (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where - Rx : HOD - Rx = Replace' (* z) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy))) ? - PxRx∋z : * z ⊆ ZFP P Rx - PxRx∋z {w} zw = subst (λ k → ZFProduct P Rx k ) ty70 ( ab-pair (zp1 b) record { z = w ; az = zw ; x=ψz = refl } ) where - a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw) - b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw ) - ty73 : & (* (zπ2 a)) ≡ zπ2 b - ty73 = begin - & (* (zπ2 a)) ≡⟨ &iso ⟩ - zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ - zπ2 b ∎ where open ≡-Reasoning - ty70 : & < * (zπ1 b) , * (& (* (zπ2 a))) > ≡ w - ty70 with zp-iso (subst (λ k → odef (ZFP P Q) k) (sym &iso) (f⊆L F az _ zw )) - ... | eq = trans (cong₂ (λ j k → & < j , * k > ) refl ty73 ) (trans eq &iso ) - ty71 : * z ⊆ ZFP P (* x) - ty71 = subst (λ k → * z ⊆ ZFP P k ) ty72 PxRx∋z where - ty72 : Rx ≡ * x - ty72 = begin - Rx ≡⟨ sym *iso ⟩ - * (& Rx) ≡⟨ cong (*) (sym x=ψz ) ⟩ - * x ∎ where open ≡-Reasoning - ty80 : Power (ZFP P Q) ∋ ZFP P (* x) - ty80 y yx = isQ→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where - ty81 : * x ⊆ Q - ty81 {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 ty84) ty87 where - a = f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1)) - (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1)) - b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) (f⊆L F az _ az1 ) - ty87 : odef Q (zπ2 b) - ty87 = zp2 b - ty84 : w ≡ (zπ2 b) - ty84 = begin - w ≡⟨ trans x=ψz1 &iso ⟩ - zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b )) ⟩ - zπ2 b ∎ where open ≡-Reasoning - + FQSet⊆F1 : {x : Ordinal } → odef (filter FQ) x → odef (filter F) (& (ZFP P (* x) )) + FQSet⊆F1 {x} fpx = FQSet⊆F is-apq F fpx uflq : UFLP TQ FQ UFQ uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ @@ -826,7 +485,7 @@ 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∋b = FPSet⊆F1 (subst (λ k → odef (filter FP) k ) &iso fp∋b ) 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 @@ -840,7 +499,7 @@ 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∋b = FQSet⊆F1 (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
--- a/src/Tychonoff1.agda Sat Jun 03 08:13:50 2023 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,196 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} -open import Level -open import Ordinals -module Tychonoff1 {n : Level } (O : Ordinals {n}) where - -open import logic -open _∧_ -open _∨_ -open Bool - -import OD -open import Relation.Nullary -open import Data.Empty -open import Relation.Binary.Core -open import Relation.Binary.Definitions -open import Relation.Binary.PropositionalEquality -import BAlgebra -open BAlgebra O -open inOrdinal O -open OD O -open OD.OD -open ODAxiom odAxiom -import OrdUtil -import ODUtil -open Ordinals.Ordinals O -open Ordinals.IsOrdinals isOrdinal -open Ordinals.IsNext isNext -open OrdUtil O -open ODUtil O - -import ODC -open ODC O - -open import filter O -open import ZProduct O --- open import maximum-filter O - -open Filter - -filter-⊆ : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → {x : HOD} → filter F ∋ x → { z : Ordinal } - → odef x z → odef (ZFP P Q) z -filter-⊆ {P} {Q} F {x} fx {z} xz = f⊆L F fx _ (subst (λ k → odef k z) (sym *iso) xz ) - -rcp : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) P (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx)) -rcp {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP1.aa ly } - -Filter-Proj1 : {P Q a : HOD } → ZFP P Q ∋ a → - (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) - → Filter {Power P} {P} (λ x → x) -Filter-Proj1 {P} {Q} pqa F = record { filter = FP ; f⊆L = fp00 ; filter1 = f1 ; filter2 = f2 } where - FP : HOD - FP = Replace' (filter F) (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx)) {P} (rcp F) - 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 - isQ→PxQ : {x : HOD} → (x⊆P : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q - isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) - fp00 : FP ⊆ Power P - fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw - ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa - f0 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q - f0 {p} {q} PQq fp p⊆q = filter1 F PQq fp p⊆q - f1 : {p q : HOD} → Power P ∋ q → FP ∋ p → p ⊆ q → FP ∋ q - f1 {p} {q} Pq record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = & (ZFP q Q) ; az = fp01 ty05 ty06 ; x=ψz = q=proj1 } where - PQq : Power (ZFP P Q) ∋ ZFP q Q - PQq z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq ) - q⊆P : q ⊆ P - q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) - p⊆P : p ⊆ P - p⊆P {w} pw = q⊆P (p⊆q pw) - p=proj1 : & p ≡ & (ZP-proj1 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az))) - p=proj1 = x=ψz - p⊆ZP : (* z) ⊆ ZFP p Q - p⊆ZP = subst (λ k → (* z) ⊆ ZFP k Q) (sym (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP - 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) az) p⊆ZP - ty06 : ZFP p Q ⊆ ZFP q Q - ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq - fp01 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q - fp01 fzp zp⊆zq = filter1 F PQq fzp zp⊆zq - q=proj1 : & q ≡ & (ZP-proj1 P Q (* (& (ZFP q Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fp01 ty05 ty06)))) - q=proj1 = cong (&) (ZP-proj1=rev (zp2 pqa) q⊆P *iso ) - f2 : {p q : HOD} → FP ∋ p → FP ∋ q → Power P ∋ (p ∩ q) → FP ∋ (p ∩ q) - f2 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq - = record { z = _ ; az = ty50 ; x=ψz = pq=proj1 } where - p⊆P : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & - (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → p ⊆ P - p⊆P {zp} {p} fzp p=proj1 {x} px with subst (λ k → odef k x) (&≡&→≡ p=proj1) px - ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa - x⊆pxq : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & - (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → * zp ⊆ ZFP p Q - x⊆pxq {zp} {p} fzp p=proj1 = subst (λ k → (* zp) ⊆ ZFP k Q) (sym (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP - 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 = 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)) - (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)) - (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 - pq=proj1 : & (p ∩ q) ≡ & (ZP-proj1 P Q (* (& (ZFP (p ∩ q) Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) ty50))) - pq=proj1 = cong (&) (ZP-proj1=rev (zp2 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) (sym *iso) pqx)) *iso ) - -Filter-Proj1-UF : {P Q : HOD } → - (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) - → (FP : Filter {Power P} {P} (λ x → x) ) → ultra-filter FP -Filter-Proj1-UF = ? - -rcf : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) (ZFP Q P) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) -rcf {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZPmirror⊆ZFPBA P Q x (filter-⊆ F fx) ly } - -Filter-sym : {P Q : HOD } → - (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) - → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) -Filter-sym {P} {Q} F = - record { filter = fqp ; f⊆L = fqp<P ; filter1 = f1 ; filter2 = f2 } where - fqp : HOD - fqp = Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf F) - fqp<P : fqp ⊆ Power (ZFP Q P) - fqp<P {z} record { z = x ; az = fx ; x=ψz = x=ψz } w xw = - ZPmirror⊆ZFPBA P Q (* x) (filter-⊆ F (subst (λ k → odef (filter F) k) (sym &iso) fx )) - (subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw) - f1 : {p q : HOD} → Power (ZFP Q P) ∋ q → fqp ∋ p → p ⊆ q → fqp ∋ q - f1 {p} {q} QPq fqp p⊆q = record { z = _ ; az = fis00 {ZPmirror Q P p p⊆ZQP } {ZPmirror Q P q q⊆ZQP } fig01 fig03 fis04 - ; x=ψz = fis05 } where - fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q - fis00 = filter1 F - q⊆ZQP : q ⊆ ZFP Q P - q⊆ZQP {x} qx = QPq _ (subst (λ k → odef k x) (sym *iso) qx) - p⊆ZQP : p ⊆ ZFP Q P - p⊆ZQP {z} px = q⊆ZQP (p⊆q px) - fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fqp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fqp)))) - fig06 = Replaced1.x=ψz fqp - fig03 : filter F ∋ ZPmirror Q P p p⊆ZQP - fig03 with Replaced1.az fqp - ... | fz = subst (λ k → odef (filter F) k ) fig07 fz where - fig07 : Replaced1.z fqp ≡ & (ZPmirror Q P p (λ {x} px → QPq x (subst (λ k → def (HOD.od k) x ) (sym *iso) (p⊆q px)))) - fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) ))))) - fig01 : Power (ZFP P Q) ∋ ZPmirror Q P q q⊆ZQP - fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP (subst (λ k → odef k x) *iso xz) - fis04 : ZPmirror Q P p (λ z → q⊆ZQP (p⊆q z)) ⊆ ZPmirror Q P q q⊆ZQP - fis04 = ZPmirror-⊆ p⊆q - fis05 : & q ≡ & (ZPmirror P Q (* (& (ZPmirror Q P q q⊆ZQP))) - (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis00 fig01 fig03 fis04)))) - fis05 = cong (&) (sym ( ZPmirror-rev (sym *iso) )) - f2 : {p q : HOD} → fqp ∋ p → fqp ∋ q → Power (ZFP Q P) ∋ (p ∩ q) → fqp ∋ (p ∩ q) - f2 {p} {q} fp fq QPpq = record { z = _ ; az = fis12 {ZPmirror Q P p p⊆ZQP} {ZPmirror Q P q q⊆ZQP} fig03 fig04 fig01 - ; x=ψz = fis05 } where - fis12 : {p q : HOD} → filter F ∋ p → filter F ∋ q → Power (ZFP P Q) ∋ (p ∩ q) → filter F ∋ (p ∩ q) - fis12 {p} {q} fp fq PQpq = filter2 F fp fq PQpq - p⊆ZQP : p ⊆ ZFP Q P - p⊆ZQP {z} px = fqp<P fp _ (subst (λ k → odef k z) (sym *iso) px) - q⊆ZQP : q ⊆ ZFP Q P - q⊆ZQP {z} qx = fqp<P fq _ (subst (λ k → odef k z) (sym *iso) qx) - pq⊆ZQP : (p ∩ q) ⊆ ZFP Q P - pq⊆ZQP {z} pqx = QPpq _ (subst (λ k → odef k z) (sym *iso) pqx) - fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fp)))) - fig06 = Replaced1.x=ψz fp - fig09 : & q ≡ & (ZPmirror P Q (* (Replaced1.z fq)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fq)))) - fig09 = Replaced1.x=ψz fq - fig03 : filter F ∋ ZPmirror Q P p p⊆ZQP - fig03 = subst (λ k → odef (filter F) k ) fig07 ( Replaced1.az fp ) where - fig07 : Replaced1.z fp ≡ & (ZPmirror Q P p p⊆ZQP ) - fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) ))))) - fig04 : filter F ∋ ZPmirror Q P q q⊆ZQP - fig04 = subst (λ k → odef (filter F) k ) fig08 ( Replaced1.az fq ) where - fig08 : Replaced1.z fq ≡ & (ZPmirror Q P q q⊆ZQP ) - fig08 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig09) ))))) - fig01 : Power (ZFP P Q) ∋ ( ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP ) - fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP (proj2 (subst (λ k → odef k x) *iso xz)) - fis05 : & (p ∩ q) ≡ & (ZPmirror P Q (* (& (ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP))) - (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis12 fig03 fig04 fig01) ))) - fis05 = cong (&) (sym ( ZPmirror-rev {Q} {P} {_} {_} {pq⊆ZQP} (trans ZPmirror-∩ (sym *iso) ) )) - -Filter-sym-UF : {P Q : HOD } → - (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) - → (FQP : Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) ) - → ultra-filter FQP -Filter-sym-UF = ? - -Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → - (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) - → Filter {Power Q} {Q} (λ x → x) -Filter-Proj2 {P} {Q} {a} pqa F = Filter-Proj1 {Q} {P} ? (Filter-sym F ) -
--- a/src/ZProduct.agda Sat Jun 03 08:13:50 2023 +0900 +++ b/src/ZProduct.agda Sat Jun 03 17:31:17 2023 +0900 @@ -267,6 +267,19 @@ zp03 : * a1 ≡ * x zp03 = proj1 (prod-≡ (&≡&→≡ eq)) +ZP-proj1-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj1 A B (* z) zab ≡ od∅ → z ≡ & od∅ +ZP-proj1-0 {A} {B} {z} {zab} eq = uf10 where + uf10 : z ≡ & od∅ + uf10 = trans (sym &iso) ( cong (&) (¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) )) where + uf11 : {y : Ordinal } → odef (* z) y → ⊥ + uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (zπ1 pqy)) eq uf12 ) ) where + pqy : odef (ZFP A B) y + pqy = zab zy + uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >) + uf14 = subst (λ k → odef (* z) k ) (sym ( zp-iso pqy)) zy + uf12 : odef (ZP-proj1 A B (* z) zab) (zπ1 pqy) + uf12 = record { b = _ ; aa = zp1 pqy ; bb = zp2 pqy ; c∋ab = uf14 } + record ZP2 (A B C : HOD) ( cab : C ⊆ ZFP A B ) (b : Ordinal) : Set n where field a : Ordinal @@ -277,6 +290,34 @@ ZP-proj2 : (A B C : HOD) → C ⊆ ZFP A B → HOD ZP-proj2 A B C cab = record { od = record { def = λ x → ZP2 A B C cab x } ; odmax = & B ; <odmax = λ lt → odef< (ZP2.bb lt) } +ZP-proj2⊆ZFP : {A B C : HOD} → {cab : C ⊆ ZFP A B} → C ⊆ ZFP A (ZP-proj2 A B C cab) +ZP-proj2⊆ZFP {A} {B} {C} {cab} {c} cc with cab cc +... | ab-pair {a} {b} aa bb = ab-pair aa record { a = _ ; aa = aa ; bb = bb ; c∋ab = cc } + +ZP-proj2=rev : {A B a m : HOD} {b : Ordinal } → {cab : m ⊆ ZFP A B} → odef A b → a ⊆ B → m ≡ ZFP A a → a ≡ ZP-proj2 A B m cab +ZP-proj2=rev {A} {B} {a} {m} {b} {cab} bb a⊆A refl = ==→o≡ record { eq→ = zp00 ; eq← = zp01 } where + zp00 : {x : Ordinal } → odef a x → ZP2 A B (ZFP A a ) cab x + zp00 {x} ax = record { a = _ ; aa = bb ; bb = a⊆A ax ; c∋ab = ab-pair bb ax } + zp01 : {x : Ordinal } → ZP2 A B (ZFP A a ) cab x → odef a x + zp01 {x} record { a = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = zp02 c∋ab refl where + zp02 : {z : Ordinal } → odef (ZFP A a ) z → z ≡ & < * b , * x > → odef a x + zp02 {.(& < * _ , * _ >)} (ab-pair {a1} {b1} aa1 bb1) eq = subst (λ k → odef a k) (*≡*→≡ zp03) bb1 where + zp03 : * b1 ≡ * x + zp03 = proj2 (prod-≡ (&≡&→≡ eq)) + +ZP-proj2-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj2 A B (* z) zab ≡ od∅ → z ≡ & od∅ +ZP-proj2-0 {A} {B} {z} {zab} eq = uf10 where + uf10 : z ≡ & od∅ + uf10 = trans (sym &iso) ( cong (&) (¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) )) where + uf11 : {y : Ordinal } → odef (* z) y → ⊥ + uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (zπ2 pqy)) eq uf12 ) ) where + pqy : odef (ZFP A B) y + pqy = zab zy + uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >) + uf14 = subst (λ k → odef (* z) k ) (sym ( zp-iso pqy)) zy + uf12 : odef (ZP-proj2 A B (* z) zab) (zπ2 pqy) + uf12 = record { a = _ ; aa = zp1 pqy ; bb = zp2 pqy ; c∋ab = uf14 } + record Func (A B : HOD) : Set n where field func : {x : Ordinal } → odef A x → Ordinal @@ -468,6 +509,44 @@ zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba') x=ba)))))) (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba') x=ba)))))) +ZPmirror-neg : {A B C D : HOD} → {cdab : (C ＼ D) ⊆ ZFP A B } {cab : C ⊆ ZFP A B } {dab : D ⊆ ZFP A B } + → ZPmirror A B (C ＼ D) cdab ≡ ZPmirror A B C cab ＼ ZPmirror A B D dab +ZPmirror-neg {A} {B} {C} {D} {cdab} {cab} {dab} = ==→o≡ record { eq→ = za08 ; eq← = za10 } where + za08 : {x : Ordinal} → ZPC A B (C ＼ D) cdab x → odef (ZPmirror A B C cab ＼ ZPmirror A B D dab) x + za08 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = + ⟪ record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = proj1 c∋ab ; x=ba = x=ba } , za09 ⟫ where + za09 : ¬ odef (ZPmirror A B D dab) x + za09 zd = ⊥-elim ( proj2 c∋ab (subst (λ k → odef D k) (sym zs02) (ZPC.c∋ab zd) ) ) where + x=ba' = ZPC.x=ba zd + zs02 : & < * a , * b > ≡ & < * (ZPC.a zd) , * (ZPC.b zd) > + zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba' ) x=ba)))))) + (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (trans (sym x=ba' ) x=ba)))))) + za10 : {x : Ordinal} → odef (ZPmirror A B C cab ＼ ZPmirror A B D dab) x → ZPC A B (C ＼ D) cdab x + za10 {x} ⟪ record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } , neg ⟫ = + record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = ⟪ c∋ab , za11 ⟫ ; x=ba = x=ba } where + za11 : ¬ odef D (& < * a , * b >) + za11 zd = ⊥-elim (neg record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = zd ; x=ba = x=ba }) + + +ZPmirror-whole : {A B : HOD} → ZPmirror A B (ZFP A B) (λ x → x) ≡ ZFP B A +ZPmirror-whole {A} {B} = ==→o≡ record { eq→ = za12 ; eq← = za13 } where + za12 : {x : Ordinal} → ZPC A B (ZFP A B) (λ x₁ → x₁) x → ZFProduct B A x + za12 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = subst (λ k → ZFProduct B A k) (sym x=ba) (ab-pair bb aa) + za13 : {x : Ordinal} → ZFProduct B A x → ZPC A B (ZFP A B) (λ x₁ → x₁) x + za13 {x} (ab-pair {b} {a} bb aa) = record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = ab-pair aa bb ; x=ba = refl } + +ZPmirror-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZPmirror A B (* z) zab ≡ od∅ → z ≡ & od∅ +ZPmirror-0 {A} {B} {z} {zab} eq = uf10 where + uf10 : z ≡ & od∅ + uf10 = trans (sym &iso) ( cong (&) (¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) )) where + uf11 : {y : Ordinal } → odef (* z) y → ⊥ + uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (& < * (zπ2 pqy) , * (zπ1 pqy) >) ) eq uf12 ) ) where + pqy : odef (ZFP A B) y + pqy = zab zy + uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >) + uf14 = subst (λ k → odef (* z) k ) (sym ( zp-iso pqy)) zy + uf12 : odef (ZPmirror A B (* z) zab) (& < * (zπ2 pqy) , * (zπ1 pqy) > ) + uf12 = record { a = _ ; b = _ ; aa = zp1 pqy ; bb = zp2 pqy ; c∋ab = uf14 ; x=ba = refl } ZFP∩ : {A B C : HOD} → ( ZFP (A ∩ B) C ≡ ZFP A C ∩ ZFP B C ) ∧ ( ZFP C (A ∩ B) ≡ ZFP C A ∩ ZFP C B ) proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/filter-util.agda Sat Jun 03 17:31:17 2023 +0900 @@ -0,0 +1,395 @@ +{-# OPTIONS --allow-unsolved-metas #-} +open import Level +open import Ordinals +module filter-util {n : Level } (O : Ordinals {n}) where + +open import logic +open _∧_ +open _∨_ +open Bool + +import OD +open import Relation.Nullary +open import Data.Empty +open import Relation.Binary.Core +open import Relation.Binary.Definitions +open import Relation.Binary.PropositionalEquality +import BAlgebra +open BAlgebra O +open inOrdinal O +open OD O +open OD.OD +open ODAxiom odAxiom +import OrdUtil +import ODUtil +open Ordinals.Ordinals O +open Ordinals.IsOrdinals isOrdinal +open Ordinals.IsNext isNext +open OrdUtil O +open ODUtil O + +import ODC +open ODC O + +open import filter O +open import ZProduct O +-- open import maximum-filter O + +open Filter + +filter-⊆ : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → {x : HOD} → filter F ∋ x → { z : Ordinal } + → odef x z → odef (ZFP P Q) z +filter-⊆ {P} {Q} F {x} fx {z} xz = f⊆L F fx _ (subst (λ k → odef k z) (sym *iso) xz ) + +rcp : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) P (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx)) +rcp {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP1.aa ly } + +Filter-Proj1 : {P Q a : HOD } → ZFP P Q ∋ a → + (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) + → Filter {Power P} {P} (λ x → x) +Filter-Proj1 {P} {Q} pqa F = record { filter = FP ; f⊆L = fp00 ; filter1 = f1 ; filter2 = f2 } where + FP : HOD + FP = Replace' (filter F) (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx)) {P} (rcp F) + 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 + isQ→PxQ : {x : HOD} → (x⊆P : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q + isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) + fp00 : FP ⊆ Power P + fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw + ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa + f0 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q + f0 {p} {q} PQq fp p⊆q = filter1 F PQq fp p⊆q + f1 : {p q : HOD} → Power P ∋ q → FP ∋ p → p ⊆ q → FP ∋ q + f1 {p} {q} Pq record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = & (ZFP q Q) ; az = fp01 ty05 ty06 ; x=ψz = q=proj1 } where + PQq : Power (ZFP P Q) ∋ ZFP q Q + PQq z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq ) + q⊆P : q ⊆ P + q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw ) + p⊆P : p ⊆ P + p⊆P {w} pw = q⊆P (p⊆q pw) + p=proj1 : & p ≡ & (ZP-proj1 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az))) + p=proj1 = x=ψz + p⊆ZP : (* z) ⊆ ZFP p Q + p⊆ZP = subst (λ k → (* z) ⊆ ZFP k Q) (sym (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP + 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) az) p⊆ZP + ty06 : ZFP p Q ⊆ ZFP q Q + ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq + fp01 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q + fp01 fzp zp⊆zq = filter1 F PQq fzp zp⊆zq + q=proj1 : & q ≡ & (ZP-proj1 P Q (* (& (ZFP q Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fp01 ty05 ty06)))) + q=proj1 = cong (&) (ZP-proj1=rev (zp2 pqa) q⊆P *iso ) + f2 : {p q : HOD} → FP ∋ p → FP ∋ q → Power P ∋ (p ∩ q) → FP ∋ (p ∩ q) + f2 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq + = record { z = _ ; az = ty50 ; x=ψz = pq=proj1 } where + p⊆P : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & + (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → p ⊆ P + p⊆P {zp} {p} fzp p=proj1 {x} px with subst (λ k → odef k x) (&≡&→≡ p=proj1) px + ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa + x⊆pxq : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & + (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → * zp ⊆ ZFP p Q + x⊆pxq {zp} {p} fzp p=proj1 = subst (λ k → (* zp) ⊆ ZFP k Q) (sym (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP + 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 = 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)) + (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)) + (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 + pq=proj1 : & (p ∩ q) ≡ & (ZP-proj1 P Q (* (& (ZFP (p ∩ q) Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) ty50))) + pq=proj1 = cong (&) (ZP-proj1=rev (zp2 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) (sym *iso) pqx)) *iso ) + +Filter-Proj1-UF : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) + → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) + → ultra-filter (Filter-Proj1 pqa F) +Filter-Proj1-UF {P} {Q} pqa F UF = record { proper = ty60 ; ultra = ty62 } where + FP = Filter-Proj1 pqa F + ty60 : ¬ (filter FP ∋ od∅) + ty60 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim (ultra-filter.proper UF + (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (subst (λ k → odef k x) (*iso) x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where + ty61 : * z ⊆ od∅ + ty61 {x} lt = ⊥-elim (¬x<0 (subst (λ k → odef k x) (trans (cong (*) (ZP-proj1-0 (sym (&≡&→≡ x=ψz)))) *iso) lt )) + ty62 : {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (filter (Filter-Proj1 pqa F) ∋ p) ∨ (filter (Filter-Proj1 pqa F) ∋ (P ＼ p)) + ty62 {p} Pp NEGP = uf05 where + p⊆P : p ⊆ P + p⊆P {z} px = Pp _ (subst (λ k → odef k z) (sym *iso) px) + mp : HOD + mp = ZFP p Q + uf03 : Power (ZFP P Q) ∋ mp + uf03 x xz with subst (λ k → odef k x ) *iso xz + ... | ab-pair ax by = ab-pair (p⊆P ax) by + uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mp) + uf04 x xz = proj1 (subst (λ k → odef k x) *iso xz) + uf02 : (filter F ∋ mp) ∨ (filter F ∋ (ZFP P Q ＼ mp)) + uf02 = ultra-filter.ultra UF uf03 uf04 + uf05 : (filter FP ∋ p) ∨ (filter FP ∋ (P ＼ p)) + uf05 with uf02 + ... | case1 fp = case1 record { z = _ ; az = fp ; x=ψz = cong (&) (ZP-proj1=rev (zp2 pqa) p⊆P *iso) } + ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = cong (&) (ZP-proj1=rev (zp2 pqa) proj1 (trans *iso (proj1 ZFP\Q)) ) } + +rcq : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) Q (λ x fx → ZP-proj2 P Q x (filter-⊆ F fx)) +rcq {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP2.bb ly } + +Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → + (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) + → Filter {Power Q} {Q} (λ x → x) +Filter-Proj2 {P} {Q} pqa F = record { filter = FQ ; f⊆L = fp00 ; filter1 = f1 ; filter2 = f2 } where + FQ : HOD + FQ = Replace' (filter F) (λ x fx → ZP-proj2 P Q x (filter-⊆ F fx)) {Q} (rcq F) + 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 + isQ→PxQ : {x : HOD} → (x⊆P : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q + isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) + fp00 : FQ ⊆ Power Q + fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw + ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb + f0 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q + f0 {p} {q} PQq fp p⊆q = filter1 F PQq fp p⊆q + f1 : {p q : HOD} → Power Q ∋ q → FQ ∋ p → p ⊆ q → FQ ∋ q + f1 {p} {q} Qq record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = & (ZFP P q) ; az = fp01 ty05 ty06 ; x=ψz = q=proj2 } where + PQq : Power (ZFP P Q) ∋ ZFP P q + PQq z zpq = isQ→PxQ {* (& q)} (Qq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP P k) (sym *iso))) zpq ) + q⊆P : q ⊆ Q + q⊆P {w} qw = Qq _ (subst (λ k → odef k w ) (sym *iso) qw ) + p⊆P : p ⊆ Q + p⊆P {w} pw = q⊆P (p⊆q pw) + p=proj2 : & p ≡ & (ZP-proj2 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az))) + p=proj2 = x=ψz + p⊆ZP : (* z) ⊆ ZFP P p + p⊆ZP = subst (λ k → (* z) ⊆ ZFP P k ) (sym (&≡&→≡ p=proj2)) ZP-proj2⊆ZFP + ty05 : filter F ∋ ZFP P p + ty05 = filter1 F (λ z wz → isQ→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP + ty06 : ZFP P p ⊆ ZFP P q + ty06 (ab-pair wp wq ) = ab-pair wp (p⊆q wq) + fp01 : filter F ∋ ZFP P p → ZFP P p ⊆ ZFP P q → filter F ∋ ZFP P q + fp01 fzp zp⊆zq = filter1 F PQq fzp zp⊆zq + q=proj2 : & q ≡ & (ZP-proj2 P Q (* (& (ZFP P q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fp01 ty05 ty06)))) + q=proj2 = cong (&) (ZP-proj2=rev (zp1 pqa) q⊆P *iso ) + f2 : {p q : HOD} → FQ ∋ p → FQ ∋ q → Power Q ∋ (p ∩ q) → FQ ∋ (p ∩ q) + f2 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq + = record { z = _ ; az = ty50 ; x=ψz = pq=proj2 } where + p⊆Q : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & + (ZP-proj2 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → p ⊆ Q + p⊆Q {zp} {p} fzp p=proj2 {x} px with subst (λ k → odef k x) (&≡&→≡ p=proj2) px + ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb + x⊆pxq : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & + (ZP-proj2 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → * zp ⊆ ZFP P p + x⊆pxq {zp} {p} fzp p=proj2 = subst (λ k → (* zp) ⊆ ZFP P k ) (sym (&≡&→≡ p=proj2)) ZP-proj2⊆ZFP + 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 + pqz : odef (ZFP P (p ∩ q) ) z + pqz = subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) )) xz + pqz1 : odef P (zπ1 pqz) + pqz1 = zp1 pqz + pqz2 : odef Q (zπ2 pqz) + pqz2 = p⊆Q fzp x=ψzp (proj1 (zp2 pqz)) + ty53 : filter F ∋ ZFP P p + ty53 = filter1 F (λ z wz → isQ→PxQ (p⊆Q 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 P q + ty52 = filter1 F (λ z wz → isQ→PxQ (p⊆Q 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 p ∩ ZFP P q ) + ty51 = filter2 F ty53 ty52 ty54 + ty50 : filter F ∋ ZFP P (p ∩ q) + ty50 = subst (λ k → filter F ∋ k ) (sym (proj2 ZFP∩)) ty51 + pq=proj2 : & (p ∩ q) ≡ & (ZP-proj2 P Q (* (& (ZFP P (p ∩ q) ))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) ty50))) + pq=proj2 = cong (&) (ZP-proj2=rev (zp1 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) (sym *iso) pqx)) *iso ) + +Filter-Proj2-UF : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) + → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) + → ultra-filter (Filter-Proj2 pqa F) +Filter-Proj2-UF {P} {Q} pqa F UF = record { proper = ty60 ; ultra = ty62 } where + FQ = Filter-Proj2 pqa F + ty60 : ¬ (filter FQ ∋ od∅) + ty60 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim (ultra-filter.proper UF + (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (subst (λ k → odef k x) (*iso) x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where + ty61 : * z ⊆ od∅ + ty61 {x} lt = ⊥-elim (¬x<0 (subst (λ k → odef k x) (trans (cong (*) (ZP-proj2-0 (sym (&≡&→≡ x=ψz)))) *iso) lt )) + ty62 : {p : HOD} → Power Q ∋ p → Power Q ∋ (Q ＼ p) → (filter (Filter-Proj2 pqa F) ∋ p) ∨ (filter (Filter-Proj2 pqa F) ∋ (Q ＼ p)) + ty62 {p} Qp NEGQ = uf05 where + p⊆Q : p ⊆ Q + p⊆Q {z} px = Qp _ (subst (λ k → odef k z) (sym *iso) px) + mq : HOD + mq = ZFP P p + uf03 : Power (ZFP P Q) ∋ mq + uf03 x xz with subst (λ k → odef k x ) *iso xz + ... | ab-pair ax by = ab-pair ax (p⊆Q by) + uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mq) + uf04 x xz = proj1 (subst (λ k → odef k x) *iso xz) + uf02 : (filter F ∋ mq) ∨ (filter F ∋ (ZFP P Q ＼ mq)) + uf02 = ultra-filter.ultra UF uf03 uf04 + uf05 : (filter FQ ∋ p) ∨ (filter FQ ∋ (Q ＼ p)) + uf05 with uf02 + ... | case1 fp = case1 record { z = _ ; az = fp ; x=ψz = cong (&) (ZP-proj2=rev (zp1 pqa) p⊆Q *iso) } + ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = cong (&) (ZP-proj2=rev (zp1 pqa) proj1 (trans *iso (proj2 ZFP\Q)) ) } + +rcf : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) (ZFP Q P) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) +rcf {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZPmirror⊆ZFPBA P Q x (filter-⊆ F fx) ly } + +Filter-sym : {P Q : HOD } → + (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) + → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) +Filter-sym {P} {Q} F = + record { filter = fqp ; f⊆L = fqp<P ; filter1 = f1 ; filter2 = f2 } where + fqp : HOD + fqp = Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf F) + fqp<P : fqp ⊆ Power (ZFP Q P) + fqp<P {z} record { z = x ; az = fx ; x=ψz = x=ψz } w xw = + ZPmirror⊆ZFPBA P Q (* x) (filter-⊆ F (subst (λ k → odef (filter F) k) (sym &iso) fx )) + (subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw) + f1 : {p q : HOD} → Power (ZFP Q P) ∋ q → fqp ∋ p → p ⊆ q → fqp ∋ q + f1 {p} {q} QPq fqp p⊆q = record { z = _ ; az = fis00 {ZPmirror Q P p p⊆ZQP } {ZPmirror Q P q q⊆ZQP } fig01 fig03 fis04 + ; x=ψz = fis05 } where + fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q + fis00 = filter1 F + q⊆ZQP : q ⊆ ZFP Q P + q⊆ZQP {x} qx = QPq _ (subst (λ k → odef k x) (sym *iso) qx) + p⊆ZQP : p ⊆ ZFP Q P + p⊆ZQP {z} px = q⊆ZQP (p⊆q px) + fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fqp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fqp)))) + fig06 = Replaced1.x=ψz fqp + fig03 : filter F ∋ ZPmirror Q P p p⊆ZQP + fig03 with Replaced1.az fqp + ... | fz = subst (λ k → odef (filter F) k ) fig07 fz where + fig07 : Replaced1.z fqp ≡ & (ZPmirror Q P p (λ {x} px → QPq x (subst (λ k → def (HOD.od k) x ) (sym *iso) (p⊆q px)))) + fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) ))))) + fig01 : Power (ZFP P Q) ∋ ZPmirror Q P q q⊆ZQP + fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP (subst (λ k → odef k x) *iso xz) + fis04 : ZPmirror Q P p (λ z → q⊆ZQP (p⊆q z)) ⊆ ZPmirror Q P q q⊆ZQP + fis04 = ZPmirror-⊆ p⊆q + fis05 : & q ≡ & (ZPmirror P Q (* (& (ZPmirror Q P q q⊆ZQP))) + (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis00 fig01 fig03 fis04)))) + fis05 = cong (&) (sym ( ZPmirror-rev (sym *iso) )) + f2 : {p q : HOD} → fqp ∋ p → fqp ∋ q → Power (ZFP Q P) ∋ (p ∩ q) → fqp ∋ (p ∩ q) + f2 {p} {q} fp fq QPpq = record { z = _ ; az = fis12 {ZPmirror Q P p p⊆ZQP} {ZPmirror Q P q q⊆ZQP} fig03 fig04 fig01 + ; x=ψz = fis05 } where + fis12 : {p q : HOD} → filter F ∋ p → filter F ∋ q → Power (ZFP P Q) ∋ (p ∩ q) → filter F ∋ (p ∩ q) + fis12 {p} {q} fp fq PQpq = filter2 F fp fq PQpq + p⊆ZQP : p ⊆ ZFP Q P + p⊆ZQP {z} px = fqp<P fp _ (subst (λ k → odef k z) (sym *iso) px) + q⊆ZQP : q ⊆ ZFP Q P + q⊆ZQP {z} qx = fqp<P fq _ (subst (λ k → odef k z) (sym *iso) qx) + pq⊆ZQP : (p ∩ q) ⊆ ZFP Q P + pq⊆ZQP {z} pqx = QPpq _ (subst (λ k → odef k z) (sym *iso) pqx) + fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fp)))) + fig06 = Replaced1.x=ψz fp + fig09 : & q ≡ & (ZPmirror P Q (* (Replaced1.z fq)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fq)))) + fig09 = Replaced1.x=ψz fq + fig03 : filter F ∋ ZPmirror Q P p p⊆ZQP + fig03 = subst (λ k → odef (filter F) k ) fig07 ( Replaced1.az fp ) where + fig07 : Replaced1.z fp ≡ & (ZPmirror Q P p p⊆ZQP ) + fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) ))))) + fig04 : filter F ∋ ZPmirror Q P q q⊆ZQP + fig04 = subst (λ k → odef (filter F) k ) fig08 ( Replaced1.az fq ) where + fig08 : Replaced1.z fq ≡ & (ZPmirror Q P q q⊆ZQP ) + fig08 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig09) ))))) + fig01 : Power (ZFP P Q) ∋ ( ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP ) + fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP (proj2 (subst (λ k → odef k x) *iso xz)) + fis05 : & (p ∩ q) ≡ & (ZPmirror P Q (* (& (ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP))) + (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis12 fig03 fig04 fig01) ))) + fis05 = cong (&) (sym ( ZPmirror-rev {Q} {P} {_} {_} {pq⊆ZQP} (trans ZPmirror-∩ (sym *iso) ) )) + +Filter-sym-UF : {P Q : HOD } → + (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) + → ultra-filter (Filter-sym F) +Filter-sym-UF {P} {Q} F UF = record { proper = uf00 ; ultra = uf01 } where + FQP = Filter-sym F + uf00 : ¬ (Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf F) ∋ od∅) + uf00 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim ( ultra-filter.proper UF (subst (λ k → odef (filter F) k) uf10 az )) where + uf10 : z ≡ & od∅ + uf10 = ZPmirror-0 (sym (&≡&→≡ x=ψz)) + uf01 : {p : HOD} → Power (ZFP Q P) ∋ p → Power (ZFP Q P) ∋ (ZFP Q P ＼ p) → + (filter FQP ∋ p) ∨ (filter FQP ∋ (ZFP Q P ＼ p)) + uf01 {p} QPp NEGP = uf05 where + p⊆ZQP : p ⊆ ZFP Q P + p⊆ZQP {z} px = QPp _ (subst (λ k → odef k z) (sym *iso) px) + mp : HOD + mp = ZPmirror Q P p p⊆ZQP + uf03 : Power (ZFP P Q) ∋ mp + uf03 x xz = ZPmirror⊆ZFPBA Q P p p⊆ZQP (subst (λ k → odef k x) *iso xz) + uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mp) + uf04 x xz = proj1 (subst (λ k → odef k x) *iso xz) + uf02 : (filter F ∋ mp) ∨ (filter F ∋ (ZFP P Q ＼ mp)) + uf02 = ultra-filter.ultra UF uf03 uf04 + uf05 : (filter FQP ∋ p) ∨ (filter FQP ∋ (ZFP Q P ＼ p)) + uf05 with uf02 + ... | case1 fp = case1 record { z = _ ; az = fp ; x=ψz = cong (&) (sym ( ZPmirror-rev (sym *iso) )) } + ... | case2 fnp = case2 record { z = _ ; az = uf06 ; x=ψz = cong (&) (sym ( ZPmirror-rev (sym *iso) )) } where + uf06 : odef (filter F) (& (ZPmirror Q P (ZFP Q P ＼ p) proj1 )) + uf06 = subst (λ k → odef (filter F) k) (cong (&) (sym (trans ZPmirror-neg + (cong (λ k → k ＼ (ZPmirror Q P p (λ {z} px → QPp z (subst (λ k → OD.def (HOD.od k) z) (sym *iso) px)))) ZPmirror-whole) ))) fnp + +-- this makes check very slow +-- Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → +-- (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) +-- → Filter {Power Q} {Q} (λ x → x) +-- Filter-Proj2 {P} {Q} {a} pqa F = Filter-Proj1 {Q} {P} qpa (Filter-sym F ) where +-- qpa : ZFP Q P ∋ < * (zπ2 pqa) , * (zπ1 pqa) > +-- qpa = ab-pair (zp2 pqa) (zp1 pqa) + +-- Filter-Proj2-UF : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) +-- → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) +-- → ultra-filter (Filter-Proj2 pqa F) +-- Filter-Proj2-UF {P} {Q} {a} pqa F UF = Filter-Proj1-UF {Q} {P} qpa (Filter-sym F) (Filter-sym-UF F UF) where +-- qpa : ZFP Q P ∋ < * (zπ2 pqa) , * (zπ1 pqa) > +-- qpa = ab-pair (zp2 pqa) (zp1 pqa) + +FPSet⊆F : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) → + (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) + → {x : Ordinal } → odef (filter (Filter-Proj1 {P} {Q} pqa F )) x → odef (filter F) (& (ZFP (* x) Q)) +FPSet⊆F {P} {Q} {a} pqa F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F uf09 (subst (λ k → odef (filter F) k) (sym &iso) az) uf08 where + uf08 : * z ⊆ ZFP (* x) Q + uf08 = subst (λ k → * z ⊆ ZFP k Q) (trans (sym *iso) (cong (*) (sym x=ψz))) ZP-proj1⊆ZFP + uf09 : Power (ZFP P Q) ∋ ZFP (* x) Q + uf09 z xqz with subst (λ k → odef k z) *iso xqz + ... | ab-pair {c} {d} xc by = ab-pair uf10 by where + uf10 : odef P c + uf10 with subst (λ k → odef k c) (sym (trans (sym *iso) (cong (*) (sym x=ψz)))) xc + ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa + +FQSet⊆F : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) → + (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) + → {x : Ordinal } → odef (filter (Filter-Proj2 {P} {Q} pqa F )) x → odef (filter F) (& (ZFP P (* x) )) +FQSet⊆F {P} {Q} {a} pqa F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F uf09 (subst (λ k → odef (filter F) k) (sym &iso) az ) uf08 where + uf08 : * z ⊆ ZFP P (* x) + uf08 = subst (λ k → * z ⊆ ZFP P k ) (trans (sym *iso) (cong (*) (sym x=ψz))) ZP-proj2⊆ZFP + uf09 : Power (ZFP P Q) ∋ ZFP P (* x) + uf09 z xpz with subst (λ k → odef k z) *iso xpz + ... | ab-pair {c} {d} ax yc = ab-pair ax uf10 where + uf10 : odef Q d + uf10 with subst (λ k → odef k d) (sym (trans (sym *iso) (cong (*) (sym x=ψz)))) yc + ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb + + +-- FQSet⊆F : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) → +-- (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) +-- → {x : Ordinal } → odef (filter (Filter-Proj2 {P} {Q} pqa F )) x → odef (filter F) (& (ZFP P (* x) )) +--FQSet⊆F {P} {Q} {a} pqa F {x} f2x = FPSet⊆F {P} {Q} {a} qpa (Filter-sym F) {x} ? where +-- qpa : ZFP Q P ∋ < * (zπ2 pqa) , * (zπ1 pqa) > +-- qpa = ab-pair (zp2 pqa) (zp1 pqa) + + + + + + + + + +