Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1293:37f28f427661
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 01 Jun 2023 22:15:17 +0900 |
| parents | f29970636e01 |
| children | 968feed7cf64 |
| files | src/BAlgebra.agda src/PFOD.agda src/Topology.agda src/Tychonoff.agda |
| diffstat | 4 files changed, 40 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/src/BAlgebra.agda Thu Jun 01 20:33:20 2023 +0900 +++ b/src/BAlgebra.agda Thu Jun 01 22:15:17 2023 +0900 @@ -72,6 +72,12 @@ ... | case1 bx = bx ... | case2 ¬bx = ⊥-elim ( proj2 ( pba ⟪ A⊆P ax , ¬bx ⟫ ) ax ) +RC＼ : {L : HOD} → RCod (Power (Union L)) (λ z → L ＼ z ) +RC＼ {L} = record { ≤COD = λ {x} lt z xz → lemm {x} lt z xz } where + lemm : {x : HOD} → (L ＼ x) ⊆ Power (Union L ) + lemm {x} ⟪ Ly , nxy ⟫ z xz = record { owner = _ ; ao = Ly ; ox = xz } + + [a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅ [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) ; eq→ = λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
--- a/src/PFOD.agda Thu Jun 01 20:33:20 2023 +0900 +++ b/src/PFOD.agda Thu Jun 01 22:15:17 2023 +0900 @@ -22,6 +22,7 @@ open OD O open OD.OD open ODAxiom odAxiom +open ODAxiom-ho< odAxiom-ho< import OrdUtil import ODUtil open Ordinals.Ordinals O
--- a/src/Topology.agda Thu Jun 01 20:33:20 2023 +0900 +++ b/src/Topology.agda Thu Jun 01 22:15:17 2023 +0900 @@ -314,7 +314,7 @@ ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where -- set of coset of X CX : {X : Ordinal} → * X ⊆ OS top → Ordinal - CX {X} ox = & ( Replace (* X) (λ z → L ＼ z )) + CX {X} ox = & ( Replace (* X) (λ z → L ＼ z ) RC＼ ) CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top CCX {X} os {x} ox with subst (λ k → odef k x) *iso ox ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06 ⟫ where -- x ≡ & (L ＼ * z) @@ -336,8 +336,8 @@ -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP) -- it means there is a finite cover -- - finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L → Subbase (Replace (* X) (λ z → L ＼ z)) o∅ - finCoverBase {X} ox oc with ODC.p∨¬p O (Subbase (Replace (* X) (λ z → L ＼ z)) o∅) + finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L → Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) o∅ + finCoverBase {X} ox oc with ODC.p∨¬p O (Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) o∅) ... | case1 sb = sb ... | case2 ¬sb = ⊥-elim (¬¬cover fip25 fip20) where ¬¬cover : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) @@ -361,7 +361,7 @@ fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 ) fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) -- create HOD from Subbase ( finite intersection ) - finCoverSet : {X : Ordinal } → (x : Ordinal) → Subbase (Replace (* X) (λ z → L ＼ z)) x → HOD + finCoverSet : {X : Ordinal } → (x : Ordinal) → Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x → HOD finCoverSet {X} x (gi rx) = ( L ＼ * x ) , ( L ＼ * x ) finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy -- @@ -371,11 +371,11 @@ -- create Finite-∪ from finCoverSet isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where - fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) + fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) fip60 x (gi rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 rx)) where fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x)) fip62 = cong₂ (λ j k → & (j , k )) *iso *iso - fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) )) + fip61 : odef (Replace (* X) (_＼_ L) RC＼ ) x → odef (* X) ( & ((L ＼ * x ) )) fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where fip34 : * z1 ⊆ L fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1 @@ -395,7 +395,7 @@ isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L) (fip70 o∅ (finCoverBase xo xcp)) where - fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x) + fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x ) → (finCoverSet {X} x sb) covers (L ＼ * x) fip70 x (gi rx) = fip73 where fip73 : ((L ＼ * x) , (L ＼ * x)) covers (L ＼ * x) -- obvious fip73 = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl @@ -454,7 +454,7 @@ ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where -- set of coset of X OX : {X : Ordinal} → * X ⊆ CS top → Ordinal - OX {X} ox = & ( Replace (* X) (λ z → L ＼ z )) + OX {X} ox = & ( Replace (* X) (λ z → L ＼ z ) RC＼) OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01)) where
--- a/src/Tychonoff.agda Thu Jun 01 20:33:20 2023 +0900 +++ b/src/Tychonoff.agda Thu Jun 01 22:15:17 2023 +0900 @@ -34,7 +34,7 @@ open import filter O open import ZProduct O open import Topology O -open import maximum-filter O +-- open import maximum-filter O open Filter open Topology @@ -190,11 +190,11 @@ -- otherwise the check requires a minute -- maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) - maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) + maxf {X} 0<X CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) - mf {X} 0<X CSX fp = MaximumFilter.mf (maxf 0<X CSX fp) + mf {X} 0<X CSX fp = ? -- MaximumFilter.mf (maxf 0<X CSX fp) ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp) - ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) + ultraf {X} 0<X CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) -- -- so it has a limit as a limit of FIP -- @@ -283,7 +283,7 @@ -- take closure of given filter elements -- CF : HOD - CF = Replace (filter F) (λ x → Cl TP x ) + CF = Replace (filter F) (λ x → Cl TP x ) {P} record { ≤COD = λ {z} {y} lt → proj1 lt } CF⊆CS : CF ⊆ CS TP CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) -- @@ -424,7 +424,7 @@ 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) )) + 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 >))) @@ -453,7 +453,7 @@ -- Projection of F FPSet : HOD - FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) ))) + 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 @@ -464,15 +464,15 @@ 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 : 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})))) + 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 _ ( λ 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 (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 ⟩ fx→px fq ≡⟨ fx→px1 aq fq ⟩ q ∎ where open ≡-Reasoning FPSet⊆PP : FPSet ⊆ Power P @@ -484,7 +484,7 @@ 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))))) + (& 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 @@ -569,7 +569,7 @@ 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))) + 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) @@ -610,7 +610,7 @@ 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→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 >))) @@ -637,7 +637,7 @@ * 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 = 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 @@ -646,15 +646,15 @@ 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 : 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})))) + 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'-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 (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 ⟩ fx→qx fq ≡⟨ fx→qx1 ap fq ⟩ q ∎ where open ≡-Reasoning FQSet⊆PP : FQSet ⊆ Power Q @@ -666,7 +666,7 @@ 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))))) + (& 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 @@ -750,7 +750,7 @@ 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))) + 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)