Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1150:fe0129c40745
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 17 Jan 2023 11:21:18 +0900 |
| parents | f8a30e568eca |
| children | 8a071bf52407 |
| files | src/BAlgebra.agda src/ODUtil.agda src/Topology.agda |
| diffstat | 3 files changed, 114 insertions(+), 101 deletions(-) [+] |
line wrap: on
line diff
--- a/src/BAlgebra.agda Mon Jan 16 22:43:09 2023 +0900 +++ b/src/BAlgebra.agda Tue Jan 17 11:21:18 2023 +0900 @@ -33,26 +33,6 @@ open _∨_ open Bool ---_∩_ : ( A B : HOD ) → HOD ---A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ; --- odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) } - -∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A) -∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ } - -_∪_ : ( A B : HOD ) → HOD -A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ; - odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where - lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B) - lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _) - lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _) - -_＼_ : ( A B : HOD ) → HOD -A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) } - -¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x ) -¬∅∋ {x} = ¬x<0 - L＼L=0 : { L : HOD } → L ＼ L ≡ od∅ L＼L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← = lem1 } ) where lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x
--- a/src/ODUtil.agda Mon Jan 16 22:43:09 2023 +0900 +++ b/src/ODUtil.agda Tue Jan 17 11:21:18 2023 +0900 @@ -46,6 +46,22 @@ lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x) lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) +∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A) +∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ } + +_∪_ : ( A B : HOD ) → HOD +A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ; + odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where + lemma : {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B) + lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _) + lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _) + +_＼_ : ( A B : HOD ) → HOD +A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) } + +¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x ) +¬∅∋ {x} = ¬x<0 + pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) ) pair-xx<xy {x} {y} = ⊆→o≤ lemma where @@ -231,3 +247,26 @@ = 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) ) + +-- ∋-irr : {X x : HOD} → (a b : X ∋ x ) → a ≡ b +-- ∋-irr {X} {x} _ _ = refl +-- is requed in +-- Replace∩ : {X P Q : HOD} → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X ) +-- → Replace' (P ∩ Q) (λ _ pq → ψ _ (P⊆X (proj1 pq ))) ≡ Replace' P (λ _ p → ψ _ (P⊆X p)) ∩ Replace' Q (λ _ q → ψ _ (Q⊆X q)) +-- Replace∩ {X} {P} {Q} {ψ} P⊆X Q⊆X = ==→o≡ record { eq→ = lem04 ; eq← = ? } where +-- lem04 : {x : Ordinal} → OD.def (od (Replace' (P ∩ Q) (λ z pq → ψ z (P⊆X (proj1 pq)) ))) x +-- → OD.def (od (Replace' P (λ z p → ψ z (P⊆X p)) ∩ Replace' Q (λ z q → ψ z (Q⊆X q)))) x +-- lem04 {x} record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ +-- record { z = _ ; az = proj1 az ; x=ψz = ? } , +-- record { z = _ ; az = proj2 az ; x=ψz = ? } ⟫ + +Repl∪ψ : {X P Q : HOD} → (ψ : (x : HOD) → X ∋ x → HOD) → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X ) → (x : HOD) → (P ∪ Q) ∋ x → HOD +Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X x (case1 p) = ψ _ (P⊆X p) +Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X x (case2 q) = ψ _ (Q⊆X q) + +Replace∪ : {X P Q : HOD} → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X ) + → Replace' (P ∪ Q) (Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X) ≡ Replace' P (λ _ p → ψ _ (P⊆X p)) ∪ Replace' Q (λ _ q → ψ _ (Q⊆X q)) +Replace∪ {X} {P} {Q} {ψ} P⊆X Q⊆X = ==→o≡ record { eq→ = ? ; eq← = ? } + + +
--- a/src/Topology.agda Mon Jan 16 22:43:09 2023 +0900 +++ b/src/Topology.agda Tue Jan 17 11:21:18 2023 +0900 @@ -60,11 +60,11 @@ open Topology Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD -Cl {L} top A A⊆L = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) } - ; odmax = & L ; <odmax = odef∧< } +Cl {L} top A A⊆L = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) } + ; odmax = & L ; <odmax = odef∧< } ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L -ClL {L} top {f} = ==→o≡ ( record { eq→ = λ {x} ic +ClL {L} top {f} = ==→o≡ ( record { eq→ = λ {x} ic → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x))) ; eq← = λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } ) @@ -76,7 +76,7 @@ g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y)) -- --- if y is in a Subbase, some element of P contains it +-- if y is in a Subbase, some element of P contains it sbp : (P : HOD) {x : Ordinal } → Subbase P x → Ordinal sbp P {x} (gi {y} px) = x @@ -92,18 +92,18 @@ record Base (L P : HOD) (u x : Ordinal) : Set n where field - b : Ordinal + b : Ordinal u⊂L : * u ⊆ L sb : Subbase P b b⊆u : * b ⊆ * u bx : odef (* b) x - x⊆L : odef L x + x⊆L : odef L x x⊆L = u⊂L (b⊆u bx) SO : (L P : HOD) → HOD SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = osuc (& L) ; <odmax = tp00 } where tp00 : {y : Ordinal} → ({x : Ordinal} → odef (* y) x → Base L P y x) → y o< osuc (& L) - tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) + tp00 {y} op = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → Base.x⊆L (op yx) )) record IsSubBase (L P : HOD) : Set (suc n) where field @@ -117,12 +117,12 @@ GeneratedTopogy L P isb = record { OS = SO L P ; OS⊆PL = tp00 ; o∪ = tp02 ; o∩ = tp01 ; OS∋od∅ = tp03 } where tp03 : {x : Ordinal } → odef (* (& od∅)) x → Base L P (& od∅) x - tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) *iso (sym &iso) 0x )) + tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) *iso (sym &iso) 0x )) tp00 : SO L P ⊆ Power L tp00 {u} ou x ux with ou ux ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊂L (b⊆u bx) tp01 : {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q) - tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) ul + tp01 {p} {q} op oq {x} ux = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) ul ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx)) ; b⊆u = tp08 ; bx = tp14 } where px : odef (* (& p)) x px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) ) @@ -131,14 +131,14 @@ b : Ordinal b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx))) tp08 : * b ⊆ * (& (p ∩ q) ) - tp08 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where + tp08 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where tp11 : * (Base.b (op px)) ⊆ * (& p ) tp11 = Base.b⊆u (op px) tp12 : * (Base.b (oq qx)) ⊆ * (& q ) tp12 = Base.b⊆u (oq qx) - tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p + tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) *iso tp11) - tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q + tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) *iso tp12) tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x tp14 = subst (λ k → odef k x ) (sym *iso) ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫ @@ -149,22 +149,22 @@ tp02 : { q : HOD} → q ⊂ SO L P → SO L P ∋ Union q tp02 {q} q⊂O {x} ux with subst (λ k → odef k x) *iso ux ... | record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx - ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) tp04 + ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) tp04 ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06 ; bx = bx } where tp05 : Union q ⊆ L tp05 {z} record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx - ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } + ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx )) tp04 : Union q ⊆ L - tp04 = tp05 + tp04 = tp05 tp06 : * b ⊆ Union q - tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } + tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz } -- Product Topology open ZFProduct --- Product Topology is not +-- Product Topology is not -- ZFP (OS TP) (OS TQ) (box) record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where @@ -196,7 +196,7 @@ pbase : {P Q : HOD} → Topology P → Topology Q → HOD pbase {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (Power (ZFP P Q)) ; <odmax = tp00 } where tp00 : {y : Ordinal} → BaseP TP Q y ∨ BaseQ P TQ y → y o< & (Power (ZFP P Q)) - tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq ) + tp00 {y} bpq = odef< ( pbase⊆PL TP TQ bpq ) ProductTopology : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q) ProductTopology {P} {Q} TP TQ = GeneratedTopogy (ZFP P Q) (pbase TP TQ) record { P⊆PL = pbase⊆PL TP TQ } @@ -215,34 +215,33 @@ record FIP {L : HOD} (top : Topology L) : Set n where field - limit : {X : Ordinal } → * X ⊆ CS top + limit : {X : Ordinal } → * X ⊆ CS top → ( { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → Ordinal - is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) - → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) + is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) + → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip) - L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) - → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) - → {x : Ordinal } → odef (* X) x + L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) + → ( fip : { C : Ordinal } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) + → {x : Ordinal } → odef (* X) x → odef L (limit CX fip) L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx) -- Compact data Finite-∪ (S : HOD) : Ordinal → Set n where - fin-∅ : Finite-∪ S o∅ - fin-e : {x : Ordinal } → odef S x → Finite-∪ S x + fin-e : {x : Ordinal } → * x ⊆ S → Finite-∪ S x fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y)) record Compact {L : HOD} (top : Topology L) : Set n where field finCover : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal isCover : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L - isFinite : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp ) + isFinite : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp ) -- FIP is Compact FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top → Compact top -FIP→Compact {L} top fip with trio< (& L) o∅ +FIP→Compact {L} top fip with trio< (& L) o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) ... | tri≈ ¬a b ¬c = record { finCover = λ _ _ → o∅ ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 } where -- L is empty @@ -251,18 +250,18 @@ fip01 : {X : Ordinal } → (xcp : * X covers L) → (* o∅) covers L fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx) ; P∋cover = λ Lx → ⊥-elim (fip02 Lx) ; isCover = λ Lx → ⊥-elim (fip02 Lx) } fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) o∅ - fip00 {X} xo xcp = fin-∅ + fip00 {X} xo xcp = fin-e ( λ {x} 0x → ⊥-elim (¬x<0 (subst (λ k → odef k x) o∅≡od∅ 0x) ) ) ... | 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 xz → L ＼ z )) - CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top + 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) fip07 : z ≡ & (L ＼ * x) fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L ＼ k )) (cong (*) (sym x=ψz))) ( cong (&) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } )) where fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) → odef (* z) x - fip08 {x} ⟪ Lx , not ⟫ with subst (λ k → (¬ odef k x)) *iso not -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥ + fip08 {x} ⟪ Lx , not ⟫ with subst (λ k → (¬ odef k x)) *iso not -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥ ... | Lx∧¬zx = ODC.double-neg-elim O ( λ nz → Lx∧¬zx ⟪ Lx , nz ⟫ ) fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) fip09 {w} zw = ⟪ os⊆L top (os (subst (λ k → odef (* X) k) (sym &iso) az)) zw , subst (λ k → ¬ odef k w) (sym *iso) fip10 ⟫ where @@ -277,71 +276,66 @@ -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP ) -- it means there is a finite cover -- - record CFIP (x : Ordinal) : Set n where + record CFIP (X x : Ordinal) : Set n where field - is-CS : * x ⊆ CS top - sx : Subbase (* x) o∅ - Cex : HOD - Cex = record { od = record { def = λ x → CFIP x } ; odmax = osuc (& (CS top)) ; <odmax = λ {x} lt → - subst₂ (λ j k → j o≤ k ) &iso refl ( ⊆→o≤ (CFIP.is-CS lt )) } - fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex =h= od∅ ) - fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where + is-CS : * x ⊆ Replace' (* X) (λ z xz → L ＼ z) + sx : Subbase (* x) o∅ + Cex : (X : Ordinal ) → HOD + Cex X = record { od = record { def = λ x → CFIP X x } ; odmax = osuc (& (Replace' (* X) (λ z xz → L ＼ z))) ; <odmax = ? } where + fip05 : {y : Ordinal} → CFIP X y → y o< osuc (& L) + fip05 {y} cf = subst₂ (λ j k → j o≤ k ) ? ? ( ⊆→o≤ ( CFIP.is-CS cf )) + fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex X =h= od∅ ) + fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where -- CX is finite intersection fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x - fip02 {C} {x} C<CX sc with trio< x o∅ + fip02 {C} {x} C<CX sc with trio< x o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) ... | tri> ¬a ¬b c = c ... | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; sx = subst (λ k → Subbase (* C) k) b sc } )) where - fip10 : * C ⊆ CS top - fip10 {w} cw = CCX ox ( C<CX cw ) - -- we have some intersection because L is not empty + fip10 : * C ⊆ Replace' (* X) (λ z xz → L ＼ z) + fip10 {w} cw = subst (λ k → odef k w) *iso ( C<CX cw ) + -- we have some intersection because L is not empty (if we have an element of L, we don't need choice) fip26 : odef (* (CX ox)) (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) ))) - fip26 = subst (λ k → odef k (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso) - record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L)) ; x=ψz = refl } + fip26 = subst (λ k → odef k (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso) + record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L)) ; x=ψz = refl } fip25 : odef L( FIP.limit fip (CCX ox) fip02 ) fip25 = FIP.L∋limit fip (CCX ox) fip02 fip26 fip20 : {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 )) fip20 {y} Xy yl = proj2 fip21 yl where fip22 : odef (* (CX ox)) (& ( L ＼ * y )) - fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } + fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl } 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 ) - fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) + fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ )) cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal - cex {X} ox oc = & ( ODC.minimal O Cex (fip00 ox oc)) - CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → CFIP (cex ox oc) - CXfip {X} ox oc = ODC.x∋minimal O Cex (fip00 ox oc) - -- - -- Subbase (* CCX) s -- Finite-∪ (* X) (replaced s) - -- sa ∩ sb ≡ s ( L ＼ sa ) ∪ (L ＼ sb) ≡ (replaced s) - -- CCX ∋ s (replaced s) ∋ ( L ＼ s ) + cex {X} ox oc = & ( ODC.minimal O (Cex X) (fip00 ox oc)) + CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → CFIP X (cex ox oc) + CXfip {X} ox oc = ODC.x∋minimal O (Cex X) (fip00 ox oc) -- - -- Subbase (* (cex ox oc)) s -- Finite-∪ (* X) (finCover xo xcp) - -- sa ∩ sb ( L ＼ sa ) ∪ (L ＼ sb) - record Cover+Int {X : Ordinal } (ox : * X ⊆ OS top) (oc : * X covers L) : Set n where - field - x w : Ordinal - is-CS : * x ⊆ CS top - x+w=L : (* x ∪ * w ) =h= L - sx : Subbase (* (cex ox oc)) w - fc : Finite-∪ (* X) x - -- -- this defines finite cover finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L ＼ z )) - -- create Finite-∪ from cex + -- create Finite-∪ from cex isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) - isFinite {X} xo xcp = ? where - fip30 : ( x y : Ordinal ) → * x ⊆ CS top → Subbase (* x) y → Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z ))) - fip30 = ? + isFinite {X} xo xcp = fip30 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp)) where + fip30 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) → Subbase (* x) y → Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z ))) + fip30 x y x⊆cs (gi sb) = fip31 where + fip31 : Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z))) + fip31 = fin-e ? + fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = ? -- is also a cover isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L - isCover1 = {!!} + isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) ? ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where + -- record { cover = λ {x} Lx → ? ; P∋cover = ? ; isCover = ? } + fip40 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) → Subbase (* x) y + → (Replace' (* x) (λ z xz → L ＼ z )) covers (L ＼ * y ) + fip40 = ? -Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top -Compact→FIP = {!!} +-- some day +Compact→FIP : Set (suc n) +Compact→FIP = {L : HOD} → (top : Topology L ) → Compact top → FIP top -- existence of Ultra Filter @@ -349,7 +343,7 @@ -- Ultra Filter has limit point -record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter {L} {P} LP ) +record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter {L} {P} LP ) (FL : filter F ∋ P) (ultra : ultra-filter F ) : Set (suc (suc n)) where field limit : Ordinal @@ -358,28 +352,28 @@ -- FIP is UFL -UFLP→FIP : {P : HOD} (TP : Topology P) → {L : HOD} (LP : L ⊆ Power P ) → +UFLP→FIP : {P : HOD} (TP : Topology P) → {L : HOD} (LP : L ⊆ Power P ) → ( (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP UFLP→FIP {P} TP {L} LP uflp = record { limit = uf00 ; is-limit = {!!} } where fip : {X : Ordinal} → * X ⊆ CS TP → Set n fip {X} CSX = {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x - F : Filter {L} {P} LP + F : {X : Ordinal} → (CSX : * X ⊆ CS TP ) → fip {X} CSX → Filter {L} {P} LP F = ? uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal - uf00 {X} CSX fip = UFLP.limit ( uflp F ? (F→ultra LP ? ? F ? ? ? ) ) - + uf00 {X} CSX fip = UFLP.limit ( uflp (F CSX fip) ? (F→ultra LP ? ? (F CSX fip) ? ? ? ) ) -FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP +-- some day +FIP→UFLP : Set (suc (suc n)) +FIP→UFLP = {P : HOD} (TP : Topology P) → FIP TP → {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F FP UF -FIP→UFLP {P} TP fip {L} LP F FP UF = ? -- product topology of compact topology is compact Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) -Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) LPQ uflp ) where +Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) LPQ uflp ) where L = pbase TP TQ LPQ = pbase⊆PL TP TQ - -- Product of UFL has limit point + -- Product of UFL has limit point uflp : (F : Filter {pbase TP TQ} LPQ) (LF : filter F ∋ ZFP P Q) (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) LPQ F LF UF - uflp F LF UF = record { limit = & < ? , {!!} > ; P∋limit = {!!} ; is-limit = {!!} } + uflp F LF UF = record { limit = & < ? , {!!} > ; P∋limit = {!!} ; is-limit = {!!} }