# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678184343 -32400
# Node ID 72b5815be24363dcae66940d1b1949977f9ba55f
# Parent  c8f5376a9623e9daa5bb017b16ff309e41e68463
...

diff -r c8f5376a9623 -r 72b5815be243 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Tue Mar 07 18:58:23 2023 +0900
+++ b/src/Tychonoff.agda	Tue Mar 07 19:19:03 2023 +0900
@@ -491,6 +491,8 @@
          uflp : UFLP TP FP UFP
          uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
 
+         --  copy and pasted, sorry
+         --
          isQ→PxQ : {x : HOD} → (x⊆Q : x ⊆ Q ) → ZFP P x  ⊆ ZFP P Q 
          isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) 
          fx→qx : {x : HOD } → filter F ∋ x → HOD 
@@ -633,19 +635,18 @@
          uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ
 
          Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
-         Pf = {!!}
-         pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → {!!} ⊆ filter F
-         pq⊆F = {!!}
+         Pf = ab-pair (UFLP.P∋limit uflp) (UFLP.P∋limit uflq)  
          isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v
-         isL {v} npq = {!!} where
+         isL {v} npq = filter1 F (λ z xz → Neighbor.v⊆P npq (subst (λ k → odef k z) *iso xz)) 
+                (subst (λ k → odef (filter F) k) (sym &iso) (F∋base pqb ?))  ? where
              bpq : Base (ZFP P Q) (pbase TP TQ) (Neighbor.u npq) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
              bpq = Neighbor.ou npq (Neighbor.ux npq)
              pqb : Subbase (pbase TP TQ) (Base.b bpq )
              pqb = Base.sb bpq
              pqb⊆opq : * (Base.b bpq) ⊆ * ( Neighbor.u npq )
              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∋base : {b : Ordinal } →  Subbase (pbase TP TQ) b → * b ⊆  * (Neighbor.u npq) → odef (filter F) b
+             F∋base (gi (case1 px)) b⊆u  = ?  where
                  -- F is ultra, so F ∋ b ∨ F ∋ (ZFP P Q ＼ b)
                  --     FP ∋ b ∨ FQ ∋ b
                  --     Neighbor b ∋ limit
@@ -655,28 +656,20 @@
                  --    x is also an elment of Proj1 F because Proj1 F has UFLP (uflp)
                  --    BaseP ∩ F is not empty
                  --    (Base P ∩ F) ⊆ F , (Base P ) ⊆ F ,
-                 il1 : odef (Power P) z ∧ ? -- ZFPproj1 (filter F) z
-                 il1 = {!!} -- UFLP.is-limit uflp ? bz
                  nei1 : HOD
                  nei1 = ? -- ZFPproj1 (* (Neighbor.u npq)) (Power P) (Power Q)
                  plimit : Ordinal
                  plimit = UFLP.limit uflp
                  nproper : {b : Ordinal } →  * b ⊆ nei1 → o∅ o< b
                  nproper = {!!}
-                 b∋z : odef nei1 z
-                 b∋z = {!!}
-                 bp : BaseP {P} TP Q z
+                 bp : BaseP {P} TP Q ?
                  bp = record { p = {!!} ; op = {!!} ; prod = {!!} }
                  neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F
                  neip = {!!}
-                 il2 : * z ⊆ ZFP (Power P) (Power Q)
-                 il2 = {!!}
                  il3 : filter F ∋ {!!}
                  il3 = {!!}
-                 fz : odef (filter F) z
-                 fz = subst (λ k → odef (filter F) k) &iso (filter1 F {!!} {!!} {!!})
-             base⊆F (gi (case2 qx)) b⊆u {z} bz = {!!}
-             base⊆F (g∩ b1 b2) b⊆u {z} bz = {!!}
+             F∋base (gi (case2 qx)) b⊆u = ?
+             F∋base (g∩ b1 b2) b⊆u = ?