# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1672453084 -32400
# Node ID 720aff4a7fa40ea5032400cc63b8e9cb3f7397e9
# Parent  f4c398c60c6758e25c401b4fb026b50e992cb287
...

diff -r f4c398c60c67 -r 720aff4a7fa4 src/Topology.agda
--- a/src/Topology.agda	Sat Dec 31 10:01:05 2022 +0900
+++ b/src/Topology.agda	Sat Dec 31 11:18:04 2022 +0900
@@ -45,6 +45,8 @@
    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} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) (sym *iso) xy  )
        -- ∈∅< ( proj1 nop )
 
 open Topology
@@ -57,14 +59,14 @@
    gi : {x : Ordinal } → odef P x → Subbase P x
    g∩ : {x y : Ordinal } → Subbase P x → Subbase P y → Subbase P (& (* x ∩ * y))
 
-Subases : (P : HOD) → HOD
-Subases P = record { od = record { def = λ x → Subbase P x } ; odmax = ? ; <odmax = ? }
+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 (Subases P) ) b
-       union : odef (Union (* b)) x
+       pb  : odef (Power (Subbases P) ) b
+       bx : odef (* b) x
 
 GeneratedTop : (P : HOD) → HOD
 GeneratedTop P = record { od = record { def = λ x → Base P x } ; odmax = & P ; <odmax = ? }
@@ -133,21 +135,34 @@
 POS : {P Q : HOD} → Topology P → Topology Q → HOD
 POS {P} {Q} TP TQ = GeneratedTop (base TP TQ)
 
+
 _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∪ = ?
+    ;  o∪ = tp13
     ;  o∩ = ?
   } 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 y z : Ordinal } → Subbase (base TP TQ) y → odef (* y) x → odef (* x) z → ZFProduct P Q z
-        tp11 {x} {y} {z} (gi (case1 record { p = p ; q = q ; op = op ; prod = prod })) yx xz = ?
-        tp11 {x} {y} {z} (gi (case2 bp)) yx xz = ?
-        tp11 {x} (g∩ {a} {b} sb sb₁) yx xz = tp11 {x} {a} sb (proj1 (subst (λ k → odef k x) *iso yx)) xz
+        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 ; union = record { owner = y ; ao = by ; ox = yx } } z xz = tp11 (pb _ by) yx xz
+        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  = record { b = ? ; pb = ? ; bx = ? } 
 
 -- existence of Ultra Filter