# HG changeset patch
# User kono
# Date 1677819334 -28800
# Node ID 2c7fb857f144e00c880f575d303c9b76714a6ccd
# Parent  83ac320583f83fcbd34aae87897543c16a6c33de
...

diff -r 83ac320583f8 -r 2c7fb857f144 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Fri Mar 03 10:42:58 2023 +0800
+++ b/src/Tychonoff.agda	Fri Mar 03 12:55:34 2023 +0800
@@ -160,28 +160,37 @@
      ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf 0<X CSX fp))
      ... | tri≈ ¬a 0=X ¬c = o∅ 
      ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-     uf02 : {X v  : Ordinal} → (0<X : o∅ o< X)  → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) 
-        → Neighbor TP (limit CSX fp) v → * v ⊆  filter ( mf CSX fp )  
-     uf02 {X} {v} 0<X CSX fp nei {x} vx with trio< o∅ X
-     ... | tri< 0<X ¬b ¬c = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)) nei vx
-     ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a 0<X )
-     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
      --
      -- the limit is an limit of entire elements of X
      --
      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 = 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 ¬b c = ⊥-elim ( ¬x<0 c )
      ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a (subst (λ k → o∅ o< k) &iso ( ∈∅< xx )))
-     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+     ... | tri< 0<X ¬b ¬c with ∨L＼X {P} {* x} {UFLP.limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp))} 
+         (UFLP.P∋limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)))
+     ... | case1 lt = lt -- odef (* x) y
+     ... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf CSX fp) uf11 ) where
+        y = UFLP.limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)) 
+        uf10 : odef (P ＼ * x ) y
+        uf10 = nlxy
+        uf03 : Neighbor TP y (& (P ＼ * x ))
+        uf03 = record { u = _ ; ou = P＼CS=OS TP (CSX (subst (λ k → odef (* X) k ) (sym &iso) xx)) 
+           ; ux = subst (λ k → odef k y) (sym *iso) uf10  
+           ; v⊆P = λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz )
+           ; u⊆v = λ x → x  } 
+        uf05 : odef (filter (MaximumFilter.mf (maxf CSX fp))) x
+        uf05 = MaximumFilter.F⊆mf (maxf CSX fp) record { b = & (* x , * x) 
+           ; b⊆X = ? ; sb = gi ?  ; u⊆P = ? ; x⊆u = λ x → x  }
+        uf06 : odef (filter (MaximumFilter.mf (maxf CSX fp))) (& (P ＼ * x ))
+        uf06 = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf 0<X CSX fp)) uf03 (subst (λ k → odef k y) (sym *iso) uf10) 
+        uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅
+        uf13 = ?
+        uf12 : odef (Power P) (& ((* x) ∩ (P ＼ * x )))
+        uf12 z pz = ?
+        uf11 : filter (MaximumFilter.mf (maxf CSX fp)) ∋ od∅
+        uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf CSX fp))) k ) uf13 
+           ( filter2 (MaximumFilter.mf (maxf CSX fp)) uf05 uf06 uf12  )
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF