--- a/src/Topology.agda	Wed Jan 18 14:09:53 2023 +0900
+++ b/src/Topology.agda	Wed Jan 18 20:53:01 2023 +0900
@@ -54,6 +54,8 @@
    CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x)  , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅  ⟫ where
         lem0 : L ＼ * (& L) ≡ od∅
         lem0 = subst (λ k → L ＼ k  ≡ od∅) (sym *iso) L＼L=0
+   CS⊆PL :  CS ⊆ Power L
+   CS⊆PL {x} Cx y xy = proj1 Cx xy 
 --- we may add
 --     OS∋L   :  OS ∋ L
 
@@ -414,22 +416,28 @@
 
 -- FIP is UFL
 
-record NFIP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (X : Ordinal) : Set n where
+record NFIP {P : HOD} (TP : Topology P) {X : Ordinal } (LP : * X ⊆ CS TP ) (u : Ordinal) : Set n where
    field
-       osx : * X ⊆ OS TP
-       fip : {u x : Ordinal} → * u ⊆ (L ＼ * X) → Subbase (* u) x → o∅ o< x
+       b x : Ordinal 
+       0<x : o∅ o< x
+       b⊆X : * b ⊆ * X
+       u⊆X : * u ⊆ * X
+       x⊆u : * x ⊆ * u
+       sb : Subbase (* b) x 
 
-UFLP→FIP : {P : HOD} (TP : Topology P) → {L : HOD} (LP : L ⊆ Power P ) →
-   ( (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP
-UFLP→FIP {P} TP {L} LP uflp = record { limit = uf00 ; is-limit = {!!} } where
+UFLP→FIP : {P : HOD} (TP : Topology P) → 
+   ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (FP : filter F ∋ P) (UF : ultra-filter F ) → UFLP TP LP F FP UF ) → FIP TP
+UFLP→FIP {P} TP uflp = record { limit = uf00 ; is-limit = {!!} } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
      fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
-     N : HOD
-     N = record { od = record { def = λ X → NFIP TP LP X } ; odmax = ? ; <odmax = ? }
-     F : Filter {L} {P} LP
-     F = record { filter = N ; f⊆L = ? ; filter1 = f1 ; filter2 = ? } where
-         f1 : {p q : HOD} → L ∋ q → N ∋ p → p ⊆ q → N ∋ q
-         f1 {p} {q} Lq record { osx = osx ; fip = fip } p⊆q = record { osx = ? ; fip = ? } 
+     N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
+     N {X} CSX fp = record { od = record { def = λ u → NFIP TP {X} CSX u } ; odmax = ? ; <odmax = ? }
+     N⊆PX : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ * X
+     N⊆PX {X} CSX fp {z} nz = ?
+     F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {* X} {P} (λ lt → CS⊆PL TP (CSX lt))
+     F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PX CSX fp ; filter1 = ? ; filter2 = ? } where
+         f1 :  {p q : HOD} → * X ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
+         f1 {p} {q} Lq Np p⊆q = ?
      uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
      uf00 {X} CSX fip = ?
      -- UFLP.limit ( uflp
@@ -445,10 +453,13 @@
 -- product topology of compact topology is compact
 
 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (ProductTopology TP TQ)
-Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) LPQ uflp ) where
+Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflp ) where
     L = pbase TP TQ
     LPQ = pbase⊆PL TP TQ
     -- Product of UFL has limit point
-    uflp : (F : Filter {pbase TP TQ} LPQ) (LF : filter F ∋ ZFP P Q) (UF : ultra-filter F)
-             → UFLP (ProductTopology TP TQ) LPQ F LF UF
-    uflp F LF UF = record { limit = & < ? , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} }
+    uflp : {L : HOD} → (LP : L ⊆ Power (ZFP P Q )) (F : Filter {L} LP) (LF : filter F ∋ ZFP P Q) (UF : ultra-filter F)
+             → UFLP (ProductTopology TP TQ) LP F LF UF
+    uflp {L} LP F LF UF = record { limit = & < ? , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} }
+
+
+