Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1235:d2506e861dbf
almost done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Mar 2023 02:31:41 +0900 |
| parents | 90e0e9fde1d6 |
| children | 59e927672b80 |
| files | src/Tychonoff.agda |
| diffstat | 1 files changed, 23 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Wed Mar 08 21:26:40 2023 +0900 +++ b/src/Tychonoff.agda Thu Mar 09 02:31:41 2023 +0900 @@ -35,7 +35,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 @@ -152,11 +152,11 @@ -- then we have maximum ultra filter -- 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) 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 i has a limit as a limit of UIP -- @@ -504,21 +504,17 @@ 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 (f⊆L F az _ zw ) ) ) where + 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 ) - ty71 : & (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)))) - ≡ zπ1 (subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw )) - ty71 = begin - & (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)))) ≡⟨ &iso ⟩ - zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)) ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ - zπ1 (subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw )) ∎ where open ≡-Reasoning - ty72 : & (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)))) - ≡ zπ1 (f⊆L F az w zw) - ty72 = ? - ty70 : & < * (& (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw))))) - , * (zπ2 (f⊆L F az w zw)) > ≡ w - ty70 = trans (cong₂ (λ j k → & < * j , k > ) ty72 refl ) (zp-iso (f⊆L F az _ 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 @@ -530,12 +526,17 @@ 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) (trans (sym &iso) (sym x=ψz1)) ty82 where - ty82 : odef P (zπ1 (f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1)) - (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1)))) - ty82 = ? - ty83 : odef P (zπ1 (f⊆L F az z1 az1)) - ty83 = zp1 (f⊆L F az _ az1 ) + ... | 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 -- copy and pasted, sorry -- @@ -687,9 +688,6 @@ Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.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 isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v isL {v} nei = filter1 F (λ z xz → Neighbor.v⊆P nei (subst (λ k → odef k z) *iso xz))