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

diff -r a839fccdef47 -r f4bccbe80540 src/Topology.agda
--- a/src/Topology.agda	Sun Jan 22 20:15:15 2023 +0900
+++ b/src/Topology.agda	Sun Jan 22 22:41:13 2023 +0900
@@ -220,24 +220,24 @@
 
 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
    field
-       p q : Ordinal
+       p : Ordinal
        op : odef (OS TP) p
        prod : x ≡ & (ZFP (* p) Q )
 
 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
    field
-       p q  : Ordinal
+       q  : Ordinal
        oq : odef (OS TQ) q
        prod : x ≡ & (ZFP P (* q ))
 
 pbase⊆PL : {P Q : HOD} → (TP : Topology P) → (TQ : Topology Q) → {x : Ordinal } → BaseP TP Q x ∨ BaseQ P TQ x → odef (Power (ZFP P Q)) x
-pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; q = q ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
+pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; 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
-pbase⊆PL {P} {Q} TP TQ {z} (case2 record { p = p ; q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
+pbase⊆PL {P} {Q} TP TQ {z} (case2 record { 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
diff -r a839fccdef47 -r f4bccbe80540 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Sun Jan 22 20:15:15 2023 +0900
+++ b/src/Tychonoff.agda	Sun Jan 22 22:41:13 2023 +0900
@@ -189,14 +189,22 @@
 
          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 = ?
-         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) (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 = ?
+         isL {v} npq {x} fx = filter2 F ? ? ? where
+             neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F 
+             neip = ?
+             neiq : {q : Ordinal } → ( bq : BaseQ P TQ q ) → * q ⊆ filter F 
+             neiq = ?
+             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 
+             base⊆F : {b : Ordinal } →  Subbase (pbase TP TQ) b → * b ⊆ filter F
+             base⊆F (gi (case1 px)) bx = ?
+             base⊆F (gi (case2 qx)) bx = ?
+             base⊆F (g∩ b1 b2) bx = filter1 F ? ? ?