# HG changeset patch
# User kono
# Date 1677811378 -28800
# Node ID 83ac320583f83fcbd34aae87897543c16a6c33de
# Parent  4d894c166762b6808da44d511ea8d494aeb38cd0
...

diff -r 4d894c166762 -r 83ac320583f8 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Fri Mar 03 08:37:02 2023 +0800
+++ b/src/Tychonoff.agda	Fri Mar 03 10:42:58 2023 +0800
@@ -43,7 +43,7 @@
 -- FIP is UFL
 
 -- filter Base
-record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
+record FBase (P : HOD ) (X : Ordinal ) (u : Ordinal) : Set n where
    field
        b x : Ordinal
        b⊆X : * b ⊆ * X
@@ -93,21 +93,20 @@
         ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt))  }
      N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P
      N⊆PP CSX fp nx b xb  = FBase.u⊆P nx xb
-     -- filter base is not empty
+     -- filter base is not empty necessary for generating ultra filter
      nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD
-     nc {X} 0<X CSX fip = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) where
-          e : HOD  -- we have an element of X
-          e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
-          Xe : odef (* X) (& e)
-          Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
+     nc {X} 0<X CSX fip = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) -- an element of X
      N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP) 
         → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) )
-     N∋nc {X} 0<X CSX fip = record { b = ? ; x =  ? ;  b⊆X = ? ; sb = ? ; u⊆P = ? ; x⊆u = ? } where
+     N∋nc {X} 0<X CSX fip = record { b = X ; x =  & e ;  b⊆X = λ x → x ; sb = gi Xe ; u⊆P = nn02 ; x⊆u = λ x → x } where
           e : HOD  -- we have an element of X
           e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
           Xe : odef (* X) (& e)
           Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
           nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) ) 
+          nn02 : * (& (nc 0<X CSX fip)) ⊆ P
+          nn02 = subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) )
+
      0<PP : o∅ o< & (Power P)
      0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where
           nn00 : odef (Power P) o∅
@@ -172,8 +171,16 @@
      --
      uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp)
      uf01 {X} CSX fp {x} xx with trio< o∅ X
-     ... | tri< 0<X ¬b ¬c = ?
-     ... | tri≈ ¬a 0=X ¬c = ?
+     ... | tri< 0<X ¬b ¬c = uf02 0<X CSX fp uf03 uf05 where
+        uf04 : Ordinal 
+        uf04 = ?
+        uf06 : Ordinal 
+        uf06 = ?
+        uf05 : odef (* uf04) uf06
+        uf05 = ?
+        uf03 : Neighbor TP (limit CSX fp) uf04
+        uf03 = record { u = ? ; ou = ? ; ux = ? ; v⊆P = ? ; u⊆v = ?  } 
+     ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a (subst (λ k → o∅ o< k) &iso ( ∈∅< xx )))
      ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP