# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1672572487 -32400
# Node ID 441ad880a45dfc90d8ea07009400b8ea0cdd1aae
# Parent  53ca3c609f0e6939de0acd86130b9b5c0953aad8
Product Topology done

diff -r 53ca3c609f0e -r 441ad880a45d src/Topology.agda
--- a/src/Topology.agda	Sun Jan 01 20:07:04 2023 +0900
+++ b/src/Topology.agda	Sun Jan 01 20:28:07 2023 +0900
@@ -195,7 +195,20 @@
 base {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
 
 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
-_Top⊗_ {P} {Q} TP TQ =  GeneratedTopogy (ZFP P Q) (base TP TQ) ?
+_Top⊗_ {P} {Q} TP TQ =  GeneratedTopogy (ZFP P Q) (base TP TQ) record { P⊆PL = tp00 } where
+    tp00 : base TP TQ ⊆ Power (ZFP P Q)
+    tp00 {z} (case1 record { p = p ; q = q ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
+        tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q))
+        tp01 w wz with subst (λ k → odef k w ) *iso wz
+        ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where
+            tp03 : odef P a
+            tp03 =  os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa
+    tp00 {z} (case2 record { p = p ; q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
+        tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) ))
+        tp01 w wz with subst (λ k → odef k w ) *iso wz
+        ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 )  where
+            tp03 : odef Q b
+            tp03 =  os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb
 
 -- existence of Ultra Filter