Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1113:384ba5a3c019
fix Topology definition
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 01 Jan 2023 13:46:38 +0900 |
| parents | fc3eea0d895d |
| children | ba3e053b85d4 |
| files | src/ODUtil.agda src/Topology.agda |
| diffstat | 2 files changed, 88 insertions(+), 78 deletions(-) [+] |
line wrap: on
line diff
--- a/src/ODUtil.agda Sat Dec 31 22:09:31 2022 +0900 +++ b/src/ODUtil.agda Sun Jan 01 13:46:38 2023 +0900 @@ -1,12 +1,12 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --allow-unsolved-metas #-} open import Level open import Ordinals module ODUtil {n : Level } (O : Ordinals {n} ) where open import zf -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) -open import Data.Nat.Properties +open import Data.Nat.Properties open import Data.Empty open import Relation.Nullary open import Relation.Binary hiding ( _⇔_ ) @@ -29,10 +29,13 @@ open _∧_ open _==_ -cseq : HOD → HOD +_⊂_ : ( A B : HOD) → Set n +_⊂_ A B = ( & A o< & B) ∧ ( A ⊆ B ) + +cseq : HOD → HOD cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x) - lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) + lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) ) @@ -43,9 +46,9 @@ pair-<xy : {x y : HOD} → {n : Ordinal} → & x o< next n → & y o< next n → & (x , y) o< next n pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y) -... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< -... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< -... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< +... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< +... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< +... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< -- another form of infinite -- pair-ord< : {x : Ordinal } → Set n @@ -57,7 +60,7 @@ lemmab1 = ho< trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C -trans-⊆ A⊆B B⊆C ab = B⊆C (A⊆B ab) +trans-⊆ A⊆B B⊆C ab = B⊆C (A⊆B ab) refl-⊆ : {A : HOD} → A ⊆ A refl-⊆ x = x @@ -76,21 +79,21 @@ subset-lemma {A} {x} = record { proj1 = λ lt x∋z → subst (λ k → odef A k ) &iso ( proj1 (lt (subst (λ k → odef x k) (sym &iso) x∋z ) )) ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫ - } + } ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅ ω<next-o∅ {y} lt = <odmax infinite lt nat→ω : Nat → HOD nat→ω Zero = od∅ -nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) +nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) ω→nato : {y : Ordinal} → infinite-d y → Nat ω→nato iφ = Zero ω→nato (isuc lt) = Suc (ω→nato lt) ω→nat : (n : HOD) → infinite ∋ n → Nat -ω→nat n = ω→nato +ω→nat n = ω→nato ω∋nat→ω : {n : Nat} → def (od infinite) (& (nat→ω n)) ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ @@ -109,10 +112,10 @@ single (case2 eq) = ==→o≡ ( ord→== (sym eq) ) single& : {x y : Ordinal } → odef (* x , * x ) y → x ≡ y -single& (case1 eq) = sym (trans eq &iso) +single& (case1 eq) = sym (trans eq &iso) single& (case2 eq) = sym (trans eq &iso) -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m pair=∨ : {a b c : Ordinal } → odef (* a , * b) c → ( a ≡ c ) ∨ ( b ≡ c ) @@ -120,20 +123,20 @@ pair=∨ {a} {b} {c} (case2 c=b) = case2 ( sym (trans c=b &iso)) ω-prev-eq1 : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y) -ω-prev-eq1 {x} {y} eq x<y with eq→ (ord→== eq) record { owner = & (* y , * y) ; ao = case2 refl +ω-prev-eq1 {x} {y} eq x<y with eq→ (ord→== eq) record { owner = & (* y , * y) ; ao = case2 refl ; ox = subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl) } -- (* x , (* x , * x)) ∋ * y ... | record { owner = u ; ao = xxx∋u ; ox = uy } with xxx∋u ... | case1 u=x = ⊥-elim ( o<> x<y (osucprev (begin - osuc y ≡⟨ sym (cong osuc &iso) ⟩ + osuc y ≡⟨ sym (cong osuc &iso) ⟩ osuc (& (* y)) ≤⟨ osucc (c<→o< {* y} {* u} uy) ⟩ -- * x ≡ * u ∋ * y - & (* u) ≡⟨ &iso ⟩ - u ≡⟨ u=x ⟩ - & (* x) ≡⟨ &iso ⟩ - x ∎ ))) where open o≤-Reasoning O + & (* u) ≡⟨ &iso ⟩ + u ≡⟨ u=x ⟩ + & (* x) ≡⟨ &iso ⟩ + x ∎ ))) where open o≤-Reasoning O ... | case2 u=xx = ⊥-elim (o<¬≡ ( begin x ≡⟨ single& (subst₂ (λ j k → odef j k ) (begin - * u ≡⟨ cong (*) u=xx ⟩ - * (& (* x , * x)) ≡⟨ *iso ⟩ + * u ≡⟨ cong (*) u=xx ⟩ + * (& (* x , * x)) ≡⟨ *iso ⟩ (* x , * x ) ∎ ) &iso uy ) ⟩ -- (* x , * x ) ∋ * y y ∎ ) x<y) where open ≡-Reasoning @@ -144,7 +147,7 @@ ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c) ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x -ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k ) (sym *iso) refl (case2 refl) } +ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k ) (sym *iso) refl (case2 refl) } ωs≠0 : (x : HOD) → ¬ ( Union ( x , (x , x)) ≡ od∅ ) ωs≠0 y eq = ⊥-elim ( ¬x<0 (subst (λ k → & y o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) ) @@ -157,17 +160,17 @@ ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x ind1 {o∅} iφ refl = sym o∅≡od∅ ind1 (isuc {x₁} ltd) ox=x = begin - nat→ω (ω→nato (isuc ltd) ) + nat→ω (ω→nato (isuc ltd) ) ≡⟨⟩ Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd))) ≡⟨ cong (λ k → Union (k , (k , k ))) lemma ⟩ Union (* x₁ , (* x₁ , * x₁)) ≡⟨ trans ( sym *iso) ox=x ⟩ - x + x ∎ where - open ≡-Reasoning + open ≡-Reasoning lemma0 : x ∋ * x₁ - lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) + lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) record { owner = & ( * x₁ , * x₁ ) ; ao = case2 refl ; ox = subst (λ k → odef k (& (* x₁))) (sym *iso) (case1 refl) } lemma1 : infinite ∋ * x₁ lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd @@ -176,7 +179,7 @@ lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) ))) lemma3 (isuc {y} ltd) iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) ))) lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq)) - ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq eq)) t + ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq eq)) t lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1 lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq) where lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1 @@ -184,10 +187,10 @@ lemma : nat→ω (ω→nato ltd) ≡ * x₁ lemma = trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd) &iso ) ) ( prev {* x₁} lemma0 lemma1 ) - -ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : infinite-d ox) → * ox ≡ nat→ω x → ω→nato ltd ≡ x -ω→nat-iso0 Zero iφ eq = refl -ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (trans (sym eq) o∅≡od∅ )) + +ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : infinite-d ox) → * ox ≡ nat→ω x → ω→nato ltd ≡ x +ω→nat-iso0 Zero iφ eq = refl +ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (trans (sym eq) o∅≡od∅ )) ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (subst (λ k → k ≡ od∅ ) *iso eq )) ω→nat-iso0 (Suc i) (isuc {x} ltd) eq = cong Suc ( ω→nat-iso0 i ltd (lemma1 eq) ) where lemma1 : * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i @@ -196,13 +199,23 @@ (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq )))))) ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i -ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso +ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso -Repl⊆ : {A B : HOD} (A⊆B : A ⊆ B) → { ψa : ( x : HOD) → A ∋ x → HOD } { ψb : ( x : HOD) → B ∋ x → HOD } +Repl⊆ : {A B : HOD} (A⊆B : A ⊆ B) → { ψa : ( x : HOD) → A ∋ x → HOD } { ψb : ( x : HOD) → B ∋ x → HOD } → ( {z : Ordinal } → (az : odef A z ) → (ψa (* z) (subst (odef A) (sym &iso) az) ≡ ψb (* z) (subst (odef B) (sym &iso) (A⊆B az)))) - → Replace' A ψa ⊆ Replace' B ψb -Repl⊆ {A} {B} A⊆B {ψa} {ψb} eq record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = A⊆B az + → Replace' A ψa ⊆ Replace' B ψb +Repl⊆ {A} {B} A⊆B {ψa} {ψb} eq record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = A⊆B az ; x=ψz = trans x=ψz (cong (&) (eq az) ) } +PPP : {P : HOD} → Power P ∋ P +PPP {P} z pz = subst (λ k → odef k z ) *iso pz +UPower⊆Q : {P Q : HOD} → P ⊆ Q → Union (Power P) ⊆ Q +UPower⊆Q {P} {Q} P⊆Q {z} record { owner = y ; ao = ppy ; ox = yz } = P⊆Q (ppy _ yz) +UPower∩ : {P : HOD} → ({ p q : HOD } → P ∋ p → P ∋ q → P ∋ (p ∩ q)) + → { p q : HOD } → Union (Power P) ∋ p → Union (Power P) ∋ q → Union (Power P) ∋ (p ∩ q) +UPower∩ {P} each {p} {q} record { owner = x ; ao = ppx ; ox = xz } record { owner = y ; ao = ppy ; ox = yz } + = record { owner = & P ; ao = PPP ; ox = lem03 } where + lem03 : odef (* (& P)) (& (p ∩ q)) + lem03 = subst (λ k → odef k (& (p ∩ q))) (sym *iso) ( each (ppx _ xz) (ppy _ yz) )
--- a/src/Topology.agda Sat Dec 31 22:09:31 2022 +0900 +++ b/src/Topology.agda Sun Jan 01 13:46:38 2023 +0900 @@ -8,12 +8,12 @@ open _∨_ open Bool -import OD -open import Relation.Nullary -open import Data.Empty +import OD +open import Relation.Nullary +open import Data.Empty open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality -import BAlgbra +import BAlgbra open BAlgbra O open inOrdinal O open OD O @@ -33,34 +33,33 @@ open import filter O open import OPair O - record Topology ( L : HOD ) : Set (suc n) where field OS : HOD - OS⊆PL : OS ⊆ Power L - o∪ : { P : HOD } → P ⊆ OS → OS ∋ Union P - o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) + OS⊆PL : OS ⊆ Power L + o∩ : { p q : HOD } → OS ∋ p → OS ∋ q → OS ∋ (p ∩ q) + o∪ : { P : HOD } → P ⊂ OS → OS ∋ Union P -- closed Set CS : HOD CS = record { od = record { def = λ x → odef OS (& ( L ＼ (* x ))) } ; odmax = & L ; <odmax = tp02 } where tp02 : {y : Ordinal } → odef OS (& (L ＼ * y)) → y o< & L tp02 {y} nop = ? - os⊆L : {x : HOD} → OS ∋ x → x ⊆ L + os⊆L : {x : HOD} → OS ∋ x → x ⊆ L os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy ) -- ∈∅< ( proj1 nop ) open Topology -- Base --- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that +-- The elements of B cover X ; For any U , V ∈ B and any point x ∈ U ∩ V there is a W ∈ B such that -- W ⊆ U ∩ V and x ∈ W . data Subbase (P : HOD) : Ordinal → Set n where gi : {x : Ordinal } → odef P x → Subbase P x g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) -Subbases : (P : HOD) → HOD -Subbases P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ; <odmax = ? } +SI : (P : HOD) → HOD +SI P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ; <odmax = ? } sbp : (P : HOD) {x : Ordinal } → Subbase P x → Ordinal sbp P {x} (gi {y} px) = x @@ -68,28 +67,26 @@ is-sbp : (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y → odef P (sbp P px ) ∧ odef (* (sbp P px)) y is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫ -is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) +is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) *iso xy)) record IsSubBase (L P : HOD) : Set (suc n) where field - P⊆PL : P ⊆ Power L + P⊆PL : P ⊆ Power L p : {x : HOD} → L ∋ x → HOD - in-P : {x : HOD} → {lx : L ∋ x } → P ∋ p lx + Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx px : {x : HOD} → {lx : L ∋ x } → p lx ∋ x GeneratedTopogy : (L P : HOD) → IsSubBase L P → Topology L -GeneratedTopogy L P isb = record { OS = Subbases P ; OS⊆PL = OS⊆PL0 ; o∪ = tp01 ; o∩ = ? } where - OS⊆PL0 : Subbases P ⊆ Power L +GeneratedTopogy L P isb = record { OS = Union (Power (SI P)) ; OS⊆PL = UPower⊆Q {SI P} {Power L} OS⊆PL0 + ; o∪ = tp01 ; o∩ = UPower∩ tp04 } where + OS⊆PL0 : SI P ⊆ Power L OS⊆PL0 (gi px) z xz = IsSubBase.P⊆PL isb px _ xz - OS⊆PL0 (g∩ {x} {y} px py) z xz = IsSubBase.P⊆PL isb (proj1 (is-sbp P px (proj1 (subst (λ k → odef k z) *iso xz )) )) _ + OS⊆PL0 (g∩ {x} {y} px py) z xz = IsSubBase.P⊆PL isb (proj1 (is-sbp P px (proj1 (subst (λ k → odef k z) *iso xz )) )) _ (proj2 (is-sbp P px (proj1 (subst (λ k → odef k z) *iso xz )) )) - tp01 : {Q : HOD} → Q ⊆ Subbases P → Subbases P ∋ Union Q - tp01 {q} qp = ε-induction0 { λ x → x ⊆ Subbases P → Subbases P ∋ Union x } tp02 q qp where - tp02 : {x : HOD} → ({y : HOD} → x ∋ y → y ⊆ Subbases P → Subbases P ∋ Union y) → x ⊆ Subbases P → Subbases P ∋ Union x - tp02 {x} prev xp = gi ? - tp04 : {p q : HOD} → Subbases P ∋ p → Subbases P ∋ q → Subbases P ∋ (p ∩ q) - tp04 {p} {q} pp pq = subst (λ k → odef (Subbases P) k ) (cong₂ (λ j k → & ( j ∩ k )) *iso *iso ) ( g∩ pp pq ) - + tp04 : {p q : HOD} → SI P ∋ p → SI P ∋ q → SI P ∋ (p ∩ q) + tp04 {p} {q} pp pq = subst (λ k → odef (SI P) k ) (cong₂ (λ j k → & ( j ∩ k )) *iso *iso ) ( g∩ pp pq ) + tp01 : {q : HOD} → q ⊂ Union (Power (SI P)) → Union (Power (SI P)) ∋ Union q + tp01 {q} ⟪ q<ups , qp ⟫ = record { owner = ? ; ao = ? ; ox = ? } -- covers @@ -124,15 +121,15 @@ -- FIP is Compact -FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top +FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top FIP→Compact {L} TL fip = record { finCover = ? ; isCover = ? ; isFinite = ? } -Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top +Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top Compact→FIP = {!!} -- Product Topology -open ZFProduct +open ZFProduct record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where field @@ -147,7 +144,7 @@ prod : x ≡ & (ZFP P (* q )) -- box : HOD --- box = ZFP (OS TP) (OS TQ) +-- box = ZFP (OS TP) (OS TQ) base : {P Q : HOD} → Topology P → Topology Q → HOD base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? } @@ -155,9 +152,9 @@ _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) _Top⊗_ {P} {Q} TP TQ = GeneratedTopogy (ZFP P Q) (base TP TQ) ? --- existence of Ultra Filter +-- existence of Ultra Filter -open Filter +open Filter -- Ultra Filter has limit point @@ -169,12 +166,12 @@ -- FIP is UFL -FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP - → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf +FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP + → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf FIP→UFLP {P} TP fip {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } -UFLP→FIP : {P : HOD} (TP : Topology P) → - ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP +UFLP→FIP : {P : HOD} (TP : Topology P) → + ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP UFLP→FIP {P} TP uflp = record { fipS⊆PL = ? ; fip≠φ = ? } -- Product of UFL has limit point (Tychonoff) @@ -184,25 +181,25 @@ uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf uflp {L} LPQ F uf = record { limit = & < * ( UFLP.limit uflpp) , ? > ; P∋limit = ? ; is-limit = ? } where - LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD + LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD LP L LPQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) LPP : (L : HOD) (LPQ : L ⊆ Power (ZFP P Q)) → LP L LPQ ⊆ Power P - LPP L LPQ record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) + LPP L LPQ record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) ) xw) where tp02 : Replace' (* z) (λ z₁ xz → * (zπ1 (LPQ (subst (odef L) (sym &iso) az) (& z₁) (subst (λ k → odef k (& z₁)) (sym *iso) xz)))) ⊆ P - tp02 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k ) (trans (sym &iso) (sym x=ψz1) ) + tp02 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k ) (trans (sym &iso) (sym x=ψz1) ) (zp1 (LPQ (subst (λ k → odef L k) (sym &iso) az) _ (tp03 az1 ))) where - tp03 : odef (* z) z1 → odef (* (& (* z))) (& (* z1)) + tp03 : odef (* z) z1 → odef (* (& (* z))) (& (* z1)) tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt) FP : Filter (LPP L LPQ) FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where tp04 : LP (filter F) (λ x → LPQ (f⊆L F x )) ⊆ LP L LPQ - tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? } + tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? } uFP : ultra-filter FP uFP = record { proper = ? ; ultra = ? } uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP uFP - uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP uFP - LQ : HOD + uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP uFP + LQ : HOD LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) ) LQQ : LQ ⊆ Power Q LQQ = ?