# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674386115 -32400
# Node ID a839fccdef47b885b758f14c4681f52cbda3a46a
# Parent  b2ca37e81ad0b2ed90e88dd6c8d60124035f3eb3
...

diff -r b2ca37e81ad0 -r a839fccdef47 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Sun Jan 22 20:04:57 2023 +0900
+++ b/src/Tychonoff.agda	Sun Jan 22 20:15:15 2023 +0900
@@ -146,14 +146,14 @@
      limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01  
      ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit
      ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01  
-     ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅ 
+     ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅  -- because limit is in CF which is a closure
      ufl03 {f} {v} ff nei fv=0 = ?
      pp :  {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x)
      pp {v} {x} nei vx z pz = ?
      ufl00 :  {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F 
      ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx))
      ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv
-     ... | case2 nfv = ?
+     ... | case2 nfv = ? -- will contradicts ufl03
 
 -- product topology of compact topology is compact
 
@@ -189,11 +189,11 @@
 
          Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
          Pf = ?
-         neip : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q  >) v → Neighbor TP p ? 
+         neip : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q  >) v → Neighbor TP (& p) ? 
          neip = ?
-         neiq : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q  >) v → Neighbor TQ q ? 
+         neiq : {v : Ordinal} → {p q : HOD} → Neighbor (ProductTopology TP TQ) (& < p , q  >) v → Neighbor TQ (& q) ? 
          neiq = ?
-         pq⊆F : {p q : HOD} → Neighbor TP p ? → Neighbor TP q ? → ? ⊆ filter F 
+         pq⊆F : {p q : HOD} → Neighbor TP (& p) (UFLP.limit uflp) → Neighbor TP (& q) (UFLP.limit uflq) → ? ⊆ filter F 
          pq⊆F = ?
          isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → * v ⊆ filter F 
          isL {v} npq {x} fx = ?