# HG changeset patch
# User kono
# Date 1677726542 -28800
# Node ID 03684784bc5fd4674f3daedb7c2a8fae22aae81c
# Parent  42000f20fdbe819a976a6436287e6f469026bd5a
...

diff -r 42000f20fdbe -r 03684784bc5f src/Tychonoff.agda
--- a/src/Tychonoff.agda	Wed Mar 01 16:34:41 2023 +0900
+++ b/src/Tychonoff.agda	Thu Mar 02 11:09:02 2023 +0800
@@ -35,7 +35,7 @@
 open import filter O
 open import OPair O
 open import Topology O
-open import maximum-filter O
+-- open import maximum-filter O
 
 open Filter  
 open Topology 
@@ -62,11 +62,30 @@
    ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP
 UFLP→FIP {P} TP uflp with trio< (& P) o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = {!!} } where
+... | tri≈ ¬a P=0 ¬c = record { limit = λ CX fip → o∅ ; is-limit = fip03 } where
    -- P is empty
    fip02 : {x : Ordinal } → ¬ odef P x
-   fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) )
-... | tri> ¬a ¬b 0<P = record { limit = ? ; is-limit = uf01 } where
+   fip02 {x} Px = ⊥-elim ( o<¬≡ (sym P=0) (∈∅< Px) )
+   fip03 : {X : Ordinal} (CX : * X ⊆ CS TP) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) {x : Ordinal} →
+            odef (* X) x → odef (* x) o∅
+   -- empty P case
+   --   if 0 < X then 0 < x ∧ P ∋ xfrom fip
+   --   if 0 ≡ X then ¬ odef X x
+   fip03 {X} CX fip {x} xx with trio< o∅ X
+   ... | tri< 0<X ¬b ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso)
+        ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx))  xe ))) where
+      0<x : o∅ o< x
+      0<x = fip (gi xx )
+      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) )
+   ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
+           * X ≡⟨ cong (*) (sym 0=X) ⟩
+           * o∅ ≡⟨  o∅≡od∅ ⟩
+           od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
+   ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → UFLP.limit (uflp (F CSX fip) (ultraf CSX fip)) ; is-limit =  ? } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
      fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x
      N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
@@ -74,12 +93,30 @@
         ; <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
-     nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → HOD
-     nc = ?
-     N∋nc :{X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → odef (N CSX fp) (& (nc CSX fp) )
-     N∋nc = ?
+     nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD
+     nc {X} CSX fip with trio< o∅ X
+     ... | tri< 0<X ¬b ¬c = 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) )
+     ... | tri≈ ¬a b ¬c = od∅
+     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+     N∋nc :{X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → odef (N CSX fip) (& (nc CSX fip) )
+     N∋nc {X} CSX fip with trio< o∅ X
+     ... | tri< 0<X ¬b ¬c = record { b = ? ; x =  ? ;  b⊆X = ? ; sb = ? ; u⊆P = ? ; x⊆u = ? } 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))) ) 
+     ... | tri≈ ¬a b ¬c = ? -- od∅
+     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
      0<PP : o∅ o< & (Power P)
-     0<PP = ?
+     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∅
+          nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt
+          ... | x<0 = ⊥-elim ( ¬x<0 x<0)
      --
      -- FIP defines a filter
      --
@@ -115,11 +152,11 @@
      -- then we have maximum ultra filter 
      --
      maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
-     maxf {X} CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp)
+     maxf {X} CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp)
      mf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
      mf {X} CSX fp =  MaximumFilter.mf (maxf CSX fp) 
      ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf CSX fp)
-     ultraf {X} CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)
+     ultraf {X} CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)
      --
      -- so i has a limit as a limit of UIP
      --
@@ -129,7 +166,7 @@
         → Neighbor TP (limit CSX fp) v → * v ⊆  filter ( mf CSX fp )  
      uf02 {X} {v} CSX fp nei {x} vx = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf CSX fp)) nei vx
      --
-     -- the limit is an element of entire elements of X
+     -- 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 ODC.∋-p O (* x) (* (limit CSX fp))
@@ -151,7 +188,7 @@
 
 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
-FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where
+FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? ; P∋limit = ? ; is-limit = ufl00 } where
      --
      -- take closure of given filter elements
      --
@@ -168,9 +205,9 @@
      -- so we have a limit
      --
      limit : Ordinal
-     limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01  
+     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  
+     ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ? -- ufl01  
      --
      -- Neigbor of limit ⊆ Filter
      --
@@ -193,7 +230,7 @@
      uflQ : (F : Filter {Power Q} {Q} (λ x → x))  (UF : ultra-filter F)
              → UFLP TQ F UF
      uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) F UF
-     -- Product of UFL has limit point
+     -- Product of UFL has a limit point
      uflPQ :  (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
              → UFLP (ProductTopology TP TQ) F UF
      uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) >  ; P∋limit = Pf ; is-limit = isL } where