Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1111:b77a7f724663

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 31 Dec 2022 22:04:23 +0900
parents 7fb6950b50f1
children fc3eea0d895d
files src/Topology.agda
diffstat 1 files changed, 23 insertions(+), 58 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Sat Dec 31 19:30:54 2022 +0900
+++ b/src/Topology.agda	Sat Dec 31 22:04:23 2022 +0900
@@ -62,24 +62,32 @@
 Subbases : (P : HOD) → HOD
 Subbases P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ; <odmax = ? }
 
-record Base (P : HOD) (x : Ordinal) : Set n where
-   field
-       b   : Ordinal
-       pb  : odef (Power (Subbases P) ) b
-       bx : odef (* b) x
+sbp :  (P : HOD) {x : Ordinal } → Subbase P x → Ordinal
+sbp P {x} (gi {y} px) = x
+sbp P {.(& (* _ ∩ * _))} (g∩ sb sb₁) = sbp P sb
 
-GeneratedTop : (P : HOD) → HOD
-GeneratedTop P = record { od = record { def = λ x → Base P x } ; odmax = & P ; <odmax = ? }
+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)) 
 
-record IsBase (L P : HOD) : Set (suc n) where
+record IsSubBase (L P : HOD) : Set (suc n) where
    field
-       p : {x : HOD} → L ∋ x → HOD
-       in-P : {x : HOD} → (lx : L ∋ x ) → P ∋ p lx
-       b∩   : {x y : HOD} → (bx : P ∋ x ) (by : P ∋ y ) → HOD
-       b∩⊂  : {x y z : HOD} → {bx : P ∋ x } {by : P ∋ y } → ( x ∩ y ) ∋  z → ( b∩ bx by ∋ x ) ∧ ( b∩ bx by  ⊆ ( x ∩ y )   )
+       P⊆PL  : P ⊆ Power L  
+       p    : {x : HOD} → L ∋ x → HOD
+       in-P : {x : HOD} → {lx : L ∋ x } → P ∋ p lx
+       px   : {x : HOD} → {lx : L ∋ x } → p lx ∋ x
 
-GeneratedIsTopogy : (P L : HOD) → IsBase L P  → Topology L
-GeneratedIsTopogy = ?
+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
+       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 )) )) _ 
+            (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 ?
+
 
 -- covers
 
@@ -142,51 +150,8 @@
 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 = ? }
 
-POS : {P Q : HOD} → Topology P → Topology Q → HOD
-POS {P} {Q} TP TQ = GeneratedTop (base TP TQ)
-
-PU : {A B : HOD} → Power A ∋ B → Power A ∋ Union B
-PU = ?
-
 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
-_Top⊗_ {P} {Q} TP TQ = record {
-       OS    = POS TP TQ
-    ;  OS⊆PL = tp10
-    ;  o∪ = tp13
-    ;  o∩ = tp14
-  } where
-        --  B : (OS P ∋ x →  proj⁻¹ x ) ∨ (OS Q ∋ y  →  proj⁻¹ y )
-        --  U ⊂ ZFP P Q  ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧  b ⊂ U )
-        tp11 : {x z : Ordinal } → Subbase (base TP TQ) z → odef (* z) x → ZFProduct P Q x
-        tp11 {x} {z} (gi (case1 record { p = p ; q = q ; op = op ; prod = z=zfp })) zx = tp12  where
-             tp12 : ZFProduct P Q x
-             tp12 with subst (λ k → odef k x) (trans (cong (*) z=zfp) *iso)  zx
-             ... | ab-pair pa qb = ZFP→ 
-                  (os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op ) (subst (λ k → odef (* p) k) (sym &iso) pa) ) 
-                  (subst (λ k → odef Q k ) (sym &iso) qb )
-        tp11 {x} {z} (gi (case2 record { p = p ; q = q ; oq = oq ; prod = z=zfp })) zx = tp12  where
-             tp12 : ZFProduct P Q x
-             tp12 with subst (λ k → odef k x) (trans (cong (*) z=zfp) *iso)  zx
-             ... | ab-pair pa qb = ZFP→  
-                  (subst (λ k → odef P k ) (sym &iso) pa ) 
-                  ((os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq )) (subst (λ k → odef (* q) k) (sym &iso) qb)  )
-        tp11 {x} (g∩ {a} {b} sb sb₁) zx = tp11 sb (proj1 (subst (λ k → odef k x) *iso zx )) 
-        tp10 : POS TP TQ ⊆ Power (ZFP P Q)
-        tp10 {x} record { b = b ; pb = pb ; bx = bx } z xz = tp11 (pb _ bx) xz
-        tp13 : {U : HOD} → U ⊆ POS TP TQ → POS TP TQ ∋ Union U
-        tp13 {U} U⊆O  = tp20 U U⊆O where
-             ind : {x : HOD} → ({y : HOD} → x ∋ y → y ⊆ POS TP TQ → POS TP TQ ∋ Union y) → x ⊆ POS TP TQ → POS TP TQ ∋ Union x
-             ind {x} prev x⊆O = record { b = & ub ; pb = ? ; bx = ? } where
-                ub : HOD
-                ub = Union ( Replace' x ( λ z xz → * (Base.b (x⊆O xz) )  ) )
-                tp14 : ub ∋ Union x
-                tp14 = ?
-             tp20 : (U : HOD ) →  U ⊆ POS TP TQ  → POS TP TQ ∋ Union U 
-             tp20 U U⊆O = ε-induction0 { λ U →  U ⊆ POS TP TQ  → POS TP TQ ∋ Union U } ind U U⊆O
-        tp14 :  {p q : HOD} → POS TP TQ ∋ p → POS TP TQ ∋ q → POS TP TQ ∋ (p ∩ q)
-        tp14 {p} {q} op oq  = record { b = & tp15 ; pb = ? ; bx = ? } where
-             tp15 : HOD
-             tp15 = ?
+_Top⊗_ {P} {Q} TP TQ =  GeneratedTopogy (ZFP P Q) (base TP TQ) ?
 
 -- existence of Ultra Filter