Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1487:1925debf28bb
Tychonoff start
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Jul 2024 16:37:12 +0900 |
| parents | 49c3ef1e9b4f |
| children | 33116eb3abd1 |
| files | src/Tychonoff.agda |
| diffstat | 1 files changed, 117 insertions(+), 83 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Mon Jul 01 16:07:57 2024 +0900 +++ b/src/Tychonoff.agda Mon Jul 01 16:37:12 2024 +0900 @@ -1,40 +1,66 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} +open import Level +open import Ordinals +open import logic +open import Relation.Nullary + open import Level open import Ordinals -module Tychonoff {n : Level } (O : Ordinals {n}) where +import HODBase +import OD +open import Relation.Nullary +module Tychonoff {n : Level } (O : Ordinals {n}) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) + (AC : OD.AxiomOfChoice O HODAxiom ) where + + +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Relation.Binary.Definitions + +open import Data.Empty + +import OrdUtil + +open Ordinals.Ordinals O +open Ordinals.IsOrdinals isOrdinal +import ODUtil open import logic +open import nat + +open OrdUtil O +open ODUtil O HODAxiom ho< + 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 HODBase._==_ + +open HODBase.ODAxiom HODAxiom +open OD O HODAxiom + +open HODBase.HOD + +open AxiomOfChoice AC +open import ODC O HODAxiom AC as ODC + +open import Level +open import Ordinals + +open import Relation.Nullary +-- open import Relation.Binary hiding ( _⇔_ ) +open import Data.Empty 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 +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +import BAlgebra -import ODC -open ODC O +open import ZProduct O HODAxiom ho< +open import filter O HODAxiom ho< AC +open import filter-util O HODAxiom ho< AC -open import filter O -open import filter-util O -open import ZProduct O -open import Topology O +import Relation.Binary.Reasoning.Setoid as EqHOD + +open import Topology O HODAxiom ho< AC open Filter open Topology @@ -108,17 +134,17 @@ -- if 0 < X then 0 < x ∧ P ∋ xfrom fip -- if 0 ≡ X then ¬ odef X x fip03 {X} CX fip {x} xx with trio< o∅ X - ... | tri< 0<X ¬b ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso) - ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx)) xe ))) where + ... | tri< 0<X ¬b ¬c = ? where -- ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso) + -- ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx)) xe ))) where 0<x : o∅ o< x 0<x = fip (gi xx ) e : HOD -- we have an element of x - e = ODC.minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) + e = minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) xe : odef (* x) (& e) - xe = ODC.x∋minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) + xe = x∋minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin * X ≡⟨ cong (*) (sym 0=X) ⟩ - * o∅ ≡⟨ o∅≡od∅ ⟩ + * o∅ ≡⟨ ? ⟩ -- o∅≡od∅ ⟩ od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit = uf01 } where @@ -131,22 +157,22 @@ N⊆PP CSX fp nx b xb = FBase.u⊆P nx xb -- filter base is not empty, it is necessary to maximize fip filter nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD - nc {X} 0<X CSX fip = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) -- an element of X + nc {X} 0<X CSX fip = minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) -- an element of X N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) ) N∋nc {X} 0<X CSX fip = record { b = X ; x = & e ; b⊆X = λ x → x ; sb = gi Xe ; u⊆P = nn02 ; x⊆u = λ x → x } where e : HOD -- we have an element of X - e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) + e = minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) Xe : odef (* X) (& e) - Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) - nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) + Xe = x∋minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) + nn01 = minimal (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) nn02 : * (& (nc 0<X CSX fip)) ⊆ P - nn02 = subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) ) + nn02 = ? -- subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) ) 0<PP : o∅ o< & (Power P) -- Power P contaisn od∅, so it is not empty 0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where nn00 : odef (Power P) o∅ - nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt + nn00 x lt with subst (λ k → odef k x) ? lt -- o∅≡od∅ lt ... | x<0 = ⊥-elim ( ¬x<0 x<0) -- -- FIP defines a filter @@ -155,32 +181,33 @@ F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where f1 : {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q = - record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp → - subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp))) } where + record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = ? -- subst (λ k → k ⊆ P) (sym *iso) f10 + ; x⊆u = λ {z} xp → ? } where + -- subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp))) } where f10 : q ⊆ P f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx )) f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q) f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where p∩q⊆p : * (& (p ∩ q)) ⊆ P - p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx )) + p∩q⊆p {x} pqx = ? -- subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx )) Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq) xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq) sbpq : Subbase (* (& Np+Nq)) (& xp∧xq) - sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl ( g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq))) + sbpq = ? -- subst₂ (λ j k → Subbase j k ) (sym *iso) refl ( g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq))) f20 : * (& Np+Nq) ⊆ * X - f20 {x} npq with subst (λ k → odef k x) *iso npq + f20 {x} npq with eq→ *iso npq ... | case1 np = FBase.b⊆X Np np ... | case2 nq = FBase.b⊆X Nq nq f22 : * (& xp∧xq) ⊆ * (& (p ∩ q)) - f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq - → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) , subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ ) + f22 = ? -- subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq + -- → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) , subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ ) -- -- it contains no empty sets becase it is a finite intersection ( Subbase (* X) x ) -- proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip {X} CSX) → ¬ (N CSX fip ∋ od∅) proper {X} CSX fip record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = u⊆P ; x⊆u = x⊆u } = o≤> x≤0 (fip (fp00 _ _ b⊆X sb)) where x≤0 : x o< osuc o∅ - x≤0 = subst₂ (λ j k → j o< osuc k) &iso (trans (cong (&) *iso) ord-od∅ ) (⊆→o≤ (x⊆u)) + x≤0 = ? -- subst₂ (λ j k → j o< osuc k) &iso (trans (cong (&) *iso) ord-od∅ ) (⊆→o≤ (x⊆u)) fp00 : (b x : Ordinal) → * b ⊆ * X → Subbase (* b) x → Subbase (* X) x fp00 b y b<X (gi by ) = gi ( b<X by ) fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz) @@ -198,6 +225,7 @@ -- 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) + postulate maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) @@ -215,12 +243,14 @@ -- -- the limit is an limit of entire elements of X -- + open BAlgebra O HODAxiom ho< P (LDec P) + uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp) uf01 {X} CSX fp {x} xx with trio< o∅ X ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a (subst (λ k → o∅ o< k) &iso ( ∈∅< xx ))) -- 0<X limit is in * x or P ＼ * x - ... | tri< 0<X ¬b ¬c with ∨L＼X {P} {* x} {UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))} + ... | tri< 0<X ¬b ¬c with ∨L＼X {* x} {UFLP.limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))} (UFLP.P∋limit ( uflp ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))) ... | case1 lt = lt -- odef (* x) y ... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf 0<X CSX fp) uf11 ) where @@ -235,16 +265,17 @@ uf10 = nlxy uf03 : Neighbor TP y (& (P ＼ * x )) uf03 = record { u = _ ; ou = P＼CS=OS TP (CSX (subst (λ k → odef (* X) k ) (sym &iso) xx)) - ; ux = subst (λ k → odef k y) (sym *iso) uf10 - ; v⊆P = λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz ) + ; ux = ? -- subst (λ k → odef k y) (sym *iso) uf10 + ; v⊆P = ? -- λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz ) ; u⊆v = λ x → x } uf07 : * (& (* x , * x)) ⊆ * X - uf07 {y} lt with subst (λ k → odef k y) *iso lt + uf07 {y} lt with eq→ *iso lt ... | case1 refl = subst (λ k → odef (* X) k ) (sym &iso) xx ... | case2 refl = subst (λ k → odef (* X) k ) (sym &iso) xx uf05 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) x uf05 = MaximumFilter.F⊆mf (maxf 0<X CSX fp) record { b = & (* x , * x) ; b⊆X = uf07 - ; sb = gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) ) ; u⊆P = x⊆P ; x⊆u = λ x → x } + ; sb = ? --- gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) ) + ; u⊆P = x⊆P ; x⊆u = λ x → x } -- if we postulate maximum filter, uf061 is an error -- uf061 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (* (& (P ＼ * x )))) -- uf061 = UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03 @@ -254,11 +285,11 @@ uf06 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (P ＼ * x )) uf06 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) &iso uf063 uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅ - uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) } ) ) where + uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ? ) where -- ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) } ) ) where uf14 : {y : Ordinal} → odef (* x ∩ (P ＼ * x)) y → odef od∅ y uf14 {y} ⟪ xy , ⟪ Px , ¬xy ⟫ ⟫ = ⊥-elim ( ¬xy xy ) uf12 : odef (Power P) (& ((* x) ∩ (P ＼ * x ))) - uf12 z pz with subst (λ k → odef k z) *iso pz + uf12 z pz with eq→ *iso pz ... | ⟪ xz , ⟪ Pz , ¬xz ⟫ ⟫ = Pz uf11 : filter (MaximumFilter.mf (maxf 0<X CSX fp)) ∋ od∅ uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k ) (trans uf13 (sym ord-od∅)) @@ -278,12 +309,12 @@ -- FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF -FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 +FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01 ; P∋limit = ufl10 ; is-limit = ufl00 } where F∋P : odef (filter F) (& P) - F∋P with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) ) (λ z az → proj1 (subst (λ k → odef k z) *iso az ) ) + F∋P with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (eq→ *iso az)) ) (λ z az → proj1 (eq→ *iso az ) ) ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp ) - ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20)) flp where + ... | case2 flp = subst (λ k → odef (filter F) k) (==→o≡ fl20) flp where fl20 : (P ＼ Ord o∅) =h= P fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) ) ⟫ } 0<P : o∅ o< & P @@ -302,10 +333,10 @@ -- it is set of closed set and has FIP ( F is proper ) -- ufl08 : {z : Ordinal} → odef (Power P) (& (Cl TP (* z))) - ufl08 {z} w zw with subst (λ k → odef k w ) *iso zw + ufl08 {z} w zw with eq→ *iso zw ... | t = proj1 t fx→px : {x : Ordinal} → odef (filter F) x → Power P ∋ * x - fx→px {x} fx z xz = f⊆L F fx _ (subst (λ k → odef k z) *iso xz ) + fx→px {x} fx z xz = f⊆L F fx _ (eq→ *iso xz ) F∋sb : {x : Ordinal} → Subbase CF x → odef (filter F) x F∋sb {x} (gi record { z = z ; az = az ; x=ψz = x=ψz }) = ufl07 where ufl09 : * z ⊆ P @@ -313,10 +344,11 @@ ufl07 : odef (filter F) x ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso)) ufl08 ) (subst (λ k → odef (filter F) k) (sym &iso) az) - (subst (λ k → * z ⊆ k ) (trans (sym *iso) (sym (cong (*) x=ψz)) ) (x⊆Clx TP {* z} ufl09 ) )) + (subst (λ k → * z ⊆ k ) ? -- (trans (sym *iso) (sym (cong (*) x=ψz)) ) + (x⊆Clx TP {* z} ufl09 ) )) F∋sb (g∩ {x} {y} sx sy) = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sx)) (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy)) - (λ z xz → fx→px (F∋sb sx) _ (subst (λ k → odef k _) (sym *iso) (proj1 (subst (λ k → odef k z) *iso xz) ))) + (λ z xz → fx→px (F∋sb sx) _ (eq← *iso (proj1 (eq→ *iso xz) ))) ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x ufl01 {x} sb = ufl04 where ufl04 : o∅ o< x @@ -326,19 +358,21 @@ begin x ≡⟨ sym b ⟩ o∅ ≡⟨ sym ord-od∅ ⟩ - & od∅ ∎ ) (F∋sb (subst (λ k → Subbase k x) *iso sb )) )) where open ≡-Reasoning + & od∅ ∎ ) ? -- (F∋sb (subst (λ k → Subbase k x) *iso sb )) + )) where open ≡-Reasoning ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) - ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01) - ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 {& P} ufl11 where + ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01) + ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01 {& P} ufl11 where ufl11 : odef (* (& CF)) (& P) - ufl11 = subst (λ k → odef k (& P)) (sym *iso) record { z = _ ; az = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) *iso) (ClL TP))) } + ufl11 = eq← *iso record { z = _ ; az = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) ? ) ? -- (ClL TP) + )) } -- -- so we have a limit -- limit : Ordinal - limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 + limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01 ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit - ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 + ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01 -- -- Neigbor of limit ⊆ Filter -- @@ -350,23 +384,23 @@ -- this contradicts ufl02 pp : {v : Ordinal} → (nei : Neighbor TP limit v ) → Power P ∋ (* (Neighbor.u nei)) pp {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } z pz - = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (subst (λ k → odef k z) *iso pz ) + = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (eq→ *iso pz ) ufl00 : {v : Ordinal} → Neighbor TP limit v → filter F ∋ * v ufl00 {v} nei with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei )) ... | case1 fu = subst (λ k → odef (filter F) k) &iso - ( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px) fu (subst (λ k → u ⊆ k ) (sym *iso) (Neighbor.u⊆v nei))) where + ( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px) fu (subst (λ k → u ⊆ k ) ? (Neighbor.u⊆v nei))) where u = * (Neighbor.u nei) px : Power P ∋ * v - px z vz = Neighbor.v⊆P nei (subst (λ k → odef k z) *iso vz ) + px z vz = Neighbor.v⊆P nei (eq→ *iso vz ) ... | case2 nfu = ⊥-elim ( ¬P\u∋limit P\u∋limit ) where u = * (Neighbor.u nei) P\u : HOD P\u = P ＼ u P\u∋limit : odef P\u limit - P\u∋limit = subst (λ k → odef k limit) *iso ( ufl02 (subst (λ k → odef k (& P\u)) (sym *iso) ufl03 )) where + P\u∋limit = eq→ *iso ( ufl02 (subst (λ k → odef k (& P\u)) ? ufl03 )) where ufl04 : & P\u ≡ & (Cl TP (* (& P\u))) - ufl04 = cong (&) (sym (trans (cong (Cl TP) *iso) - (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) ))))) + ufl04 = cong (&) (sym (trans (cong (Cl TP) ? ) ? )) + -- (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) ))))) ufl03 : odef CF (& P\u ) ufl03 = record { z = _ ; az = nfu ; x=ψz = ufl04 } ¬P\u∋limit : ¬ odef P\u limit @@ -397,9 +431,9 @@ → UFLP (ProductTopology TP TQ) F UF uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) > ; P∋limit = Pf ; is-limit = isL } where F∋PQ : odef (filter F) (& (ZFP P Q)) - F∋PQ with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) ) (λ z az → proj1 (subst (λ k → odef k z) *iso az ) ) + F∋PQ with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (eq→ *iso az)) ) (λ z az → proj1 (eq→ *iso az ) ) ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp ) - ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20)) flp where + ... | case2 flp = subst (λ k → odef (filter F) k) (==→o≡ fl20) flp where fl20 : (ZFP P Q ＼ Ord o∅) =h= ZFP P Q fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) ) ⟫ } 0<PQ : o∅ o< & (ZFP P Q) @@ -408,15 +442,15 @@ ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋PQ) ) ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) apq : HOD - apq = ODC.minimal O (ZFP P Q) (0<P→ne 0<PQ) + apq = minimal (ZFP P Q) (0<P→ne 0<PQ) is-apq : ZFP P Q ∋ apq - is-apq = ODC.x∋minimal O (ZFP P Q) (0<P→ne 0<PQ) + is-apq = x∋minimal (ZFP P Q) (0<P→ne 0<PQ) ap : odef P ( zπ1 is-apq ) 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) + F⊆pxq {x} fx {y} xy = f⊆L F fx y (eq← *iso xy) --- --- FP is a P-projection of F, which is a ultra filter @@ -448,7 +482,7 @@ Pf = ab-pair (UFLP.P∋limit uflp) (UFLP.P∋limit uflq) 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)) + isL {v} nei = filter1 F (λ z xz → Neighbor.v⊆P nei (eq→ *iso xz)) (subst (λ k → odef (filter F) k) (sym &iso) (F∋base pqb b∋l )) bpq⊆v where -- -- Product Topolgy's open set contains a subbase which is an element of ZPF p Q or ZPF P q @@ -473,13 +507,13 @@ -- subbase of product topology which includes lim is in FP, so in F -- isl00 : odef (ZFP (* (BaseP.p px)) Q) lim - isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseP.prod px)) *iso ) bl + isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseP.prod px)) ? ) bl px∋limit : odef (* (BaseP.p px)) (UFLP.limit uflp) px∋limit = isl01 isl00 refl where isl01 : {x : Ordinal } → odef (ZFP (* (BaseP.p px)) Q) x → x ≡ lim → odef (* (BaseP.p px)) (UFLP.limit uflp) isl01 (ab-pair {a} {b} bx qx) ab=lim = subst (λ k → odef (* (BaseP.p px)) k) a=lim bx where a=lim : a ≡ UFLP.limit uflp - a=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) ))) + a=lim = subst₂ (λ j k → j ≡ k ) &iso &iso ? -- (cong (&) (proj1 ( prod-≡ (subst₂ (λ j k → j ≡ k ) ? ? (cong (*) ab=lim) ) ))) fp∋b : filter FP ∋ * (BaseP.p px) 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 } @@ -487,13 +521,13 @@ 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 + isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseQ.prod qx)) ? ) bl qx∋limit : odef (* (BaseQ.q qx)) (UFLP.limit uflq) qx∋limit = isl01 isl00 refl where isl01 : {x : Ordinal } → odef (ZFP P (* (BaseQ.q qx)) ) x → x ≡ lim → odef (* (BaseQ.q qx)) (UFLP.limit uflq) isl01 (ab-pair {a} {b} px bx) ab=lim = subst (λ k → odef (* (BaseQ.q qx)) k) b=lim bx where b=lim : b ≡ UFLP.limit uflq - b=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) ))) + b=lim = ? -- subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) ))) fp∋b : filter FQ ∋ * (BaseQ.q qx) 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 } @@ -502,9 +536,9 @@ F∋base (g∩ {x} {y} b1 b2) bl = F∋x∩y where -- filter contains finite intersection fb01 : odef (filter F) x - fb01 = F∋base b1 (proj1 (subst (λ k → odef k lim) *iso bl)) + fb01 = F∋base b1 (proj1 (eq→ *iso bl)) fb02 : odef (filter F) y - fb02 = F∋base b2 (proj2 (subst (λ k → odef k lim) *iso bl)) + fb02 = F∋base b2 (proj2 (eq→ *iso bl)) F∋x∩y : odef (filter F) (& (* x ∩ * y)) F∋x∩y = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) fb01) (subst (λ k → odef (filter F) k) (sym &iso) fb02) (CAP (ZFP P Q) (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb01))