--- a/src/Topology.agda	Sat Dec 31 00:28:24 2022 +0900
+++ b/src/Topology.agda	Sat Dec 31 10:01:05 2022 +0900
@@ -49,6 +49,27 @@
 
 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 
+-- 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))
+
+Subases : (P : HOD) → HOD
+Subases 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
+
+GeneratedTop : (P : HOD) → HOD
+GeneratedTop P = record { od = record { def = λ x → Base P x } ; odmax = & P ; <odmax = ? }
+
+-- covers
 
 record _covers_ ( P q : HOD  ) : Set (suc n) where
    field
@@ -56,15 +77,6 @@
        P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
        isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x
 
--- 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 
--- W ⊆ U ∩ V and x ∈ W .
-
-data genTop (P : HOD) : HOD → Set (suc n) where
-   gi : {x : HOD} → P ∋ x → genTop P x
-   g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y)
-   g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q)
-
 -- Finite Intersection Property
 
 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
@@ -112,17 +124,14 @@
        oq : odef (OS TQ) q
        prod : x ≡ & (ZFP P (* q ))
 
+-- box : HOD
+-- 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 = ? }
 
-record BU {P Q : HOD} (TP : Topology P) (TQ : Topology Q) (x : Ordinal ) : Set n where
-   field
-       b  : Ordinal
-       pb : odef (Power (base TP TQ)) b
-       pu : odef (Union (* b)) x 
-
 POS : {P Q : HOD} → Topology P → Topology Q → HOD
-POS {P} {Q} TP TQ = record { od = record { def = λ x → BU TP TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
+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 {
@@ -131,16 +140,14 @@
     ;  o∪ = ?
     ;  o∩ = ?
   } where
-        box : HOD
-        box = ZFP (OS TP) (OS TQ) 
         --  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
         tp10 : POS TP TQ ⊆ Power (ZFP P Q)
-        tp10 {x} record { b = b ; pb = pb ; pu = record { owner = z ; ao = bz ; ox = zx } } y xy = tp11 where
-             tp11 : odef (ZFP P Q) y
-             tp11 with pb _ bz
-             ... | case1 record { p = p ; q = q ; op = op ; prod = prod } = ?
-             ... | case2 x =  ?
+        tp10 {x} record { b = b ; pb = pb ; union = record { owner = y ; ao = by ; ox = yx } } z xz = tp11 (pb _ by) yx xz
 
 -- existence of Ultra Filter