Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1223:4b6c3ed64dd1
...
| author | kono |
|---|---|
| date | Tue, 07 Mar 2023 12:13:21 +0900 |
| parents | 9f955d49e162 |
| children | e1a1161df14c |
| files | src/OD.agda src/Tychonoff.agda src/ZProduct.agda |
| diffstat | 3 files changed, 36 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OD.agda Tue Mar 07 09:00:03 2023 +0900 +++ b/src/OD.agda Tue Mar 07 12:13:21 2023 +0900 @@ -220,6 +220,9 @@ ∅< {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d ∅< {x} {y} d eq | lift () +¬x∋y→x≡od∅ : { x : HOD } → ({y : Ordinal } → ¬ odef x y ) → x ≡ od∅ +¬x∋y→x≡od∅ {x} nxy = ==→o≡ record { eq→ = λ {y} lt → ⊥-elim (nxy lt) ; eq← = λ {y} lt → ⊥-elim (¬x<0 lt) } + 0<P→ne : { x : HOD } → o∅ o< & x → ¬ ( od x == od od∅ ) 0<P→ne {x} 0<x eq = ⊥-elim ( o<¬≡ (sym (=od∅→≡o∅ eq)) 0<x )
--- a/src/Tychonoff.agda Tue Mar 07 09:00:03 2023 +0900 +++ b/src/Tychonoff.agda Tue Mar 07 12:13:21 2023 +0900 @@ -348,10 +348,11 @@ ap = zp1 is-apq aq : odef Q ( zπ2 is-apq ) aq = zp2 is-apq + 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 isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q - 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) 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 @@ -379,8 +380,6 @@ 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 - - FPSet : HOD FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) ))) FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋ ZFP q Q → FPSet ∋ q @@ -407,12 +406,12 @@ ... | 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 → + 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=F x p fx → * x ⊆ ZFP p Q + 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 >))) @@ -429,7 +428,7 @@ 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 : 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 )) ) @@ -474,9 +473,29 @@ ty51 = filter2 F ty53 ty52 ty54 ty50 : filter F ∋ ZFP (p ∩ q) Q ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51 - + ZFP\Q : {P Q p : HOD} → ( ZFP P Q ＼ ZFP p Q ) ≡ ZFP (P ＼ p) Q + ZFP\Q {P} {Q} {p} = ==→o≡ record { eq→ = ty70 ; eq← = ty71 } where + ty70 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP p Q ) x → odef (ZFP (P ＼ p) Q) x + ty70 ⟪ ab-pair {a} {b} Pa pb , npq ⟫ = ab-pair ty72 pb where + ty72 : odef (P ＼ p ) a + ty72 = ⟪ Pa , (λ pa → npq (ab-pair pa pb ) ) ⟫ + ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x + ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb + , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫ UFP : ultra-filter FP - UFP = record { proper = {!!} ; ultra = {!!} } + 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)) ? + ... | 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 (&) ZFP\Q) fnp )) uflp : UFLP TP FP UFP uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
--- a/src/ZProduct.agda Tue Mar 07 09:00:03 2023 +0900 +++ b/src/ZProduct.agda Tue Mar 07 12:13:21 2023 +0900 @@ -189,6 +189,10 @@ zz11 : & < * (zπ1 pab) , * (zπ2 pab) > ≡ & < * a , * b > zz11 = zp-iso pab +zp-iso0 : { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (zπ1 p ≡ a) ∧ (zπ2 p ≡ b) +zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) )) + , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (zp-iso1 pab) ) ) ⟫ + ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)