--- a/src/Topology.agda	Sat Dec 31 17:56:01 2022 +0900
+++ b/src/Topology.agda	Sat Dec 31 19:30:54 2022 +0900
@@ -71,6 +71,16 @@
 GeneratedTop : (P : HOD) → HOD
 GeneratedTop P = record { od = record { def = λ x → Base P x } ; odmax = & P ; <odmax = ? }
 
+record IsBase (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 )   )
+
+GeneratedIsTopogy : (P L : HOD) → IsBase L P  → Topology L
+GeneratedIsTopogy = ?
+
 -- covers
 
 record _covers_ ( P q : HOD  ) : Set (suc n) where
@@ -135,6 +145,8 @@
 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 {
@@ -164,7 +176,11 @@
         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 = ? ; pb = ? ; bx = ? }
+             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)