# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678101180 -32400
# Node ID 0e8306b146f6de1d801813419b7c3b9093bb0a01
# Parent  a8253c91f6307df85fa46c94cab3352c324cd2dd
...

diff -r a8253c91f630 -r 0e8306b146f6 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Mon Mar 06 15:23:17 2023 +0900
+++ b/src/Tychonoff.agda	Mon Mar 06 20:13:00 2023 +0900
@@ -451,13 +451,13 @@
                   x⊆pxq : * ? ⊆ ZFP p Q
                   x⊆pxq = ?
                   ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q)
-                  ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso ty55) (ab-pair ty551 ty552 ) where
-                     ty55 :  odef (ZFP (p ∩ q) Q)  z
-                     ty55 = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) ))  xz
-                     ty551 :  odef P (zπ1 ty55)
-                     ty551 = ?
-                     ty552 :  odef Q (zπ2 ty55)
-                     ty552 = ?
+                  ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where
+                     pqz :  odef (ZFP (p ∩ q) Q)  z
+                     pqz = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) ))  xz
+                     pqz1 :  odef P (zπ1 pqz)
+                     pqz1 = ?
+                     pqz2 :  odef Q (zπ2 pqz)
+                     pqz2 = ?
                   ty53 : filter F ∋ ZFP p Q 
                   ty53 = filter1 F (λ z wz → isP→PxQ ? (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) ? ) x⊆pxq
                   ty52 : filter F ∋ ZFP q Q 
@@ -494,6 +494,10 @@
              pqb⊆opq = Base.b⊆u bpq
              base⊆F : {b : Ordinal } →  Subbase (pbase TP TQ) b → * b ⊆  * (Neighbor.u npq) → * b ⊆ filter F
              base⊆F (gi (case1 px)) b⊆u {z} bz = fz  where
+                 -- F is ultra, so F ∋ b ∨ F ∋ (ZFP P Q ＼ b)
+                 --     FP ∋ b ∨ FQ ∋ b
+                 --     Neighbor b ∋ limit
+                 --  F ∋ (ZFP P Q ＼ b) → ¬  Neighbor b ∋ limit → ⊥
                  -- F contains no od∅, because it projection contains no od∅
                  --    x is an element of BaseP, which is a subset of Neighbor npq
                  --    x is also an elment of Proj1 F because Proj1 F has UFLP (uflp)