# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674385497 -32400
# Node ID b2ca37e81ad0b2ed90e88dd6c8d60124035f3eb3
# Parent  46dc298bdd77aa3d875d8180d5d0a5c751697497
...

diff -r 46dc298bdd77 -r b2ca37e81ad0 src/Topology.agda
--- a/src/Topology.agda	Sun Jan 22 10:38:52 2023 +0900
+++ b/src/Topology.agda	Sun Jan 22 20:04:57 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 open import Level
 open import Ordinals
 module Topology {n : Level } (O : Ordinals {n})   where
@@ -447,8 +449,6 @@
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
 Compact→FIP = ?
 
--- existence of Ultra Filter
-
 open Filter
 
 -- Ultra Filter has limit point
@@ -459,19 +459,12 @@
        ou : odef (OS TP) u
        ux : odef (* u) x
        v⊆P : * v ⊆ P
-       o⊆u : * u ⊆ * v
-
-record UFLP {P : HOD} (TP : Topology P)  (F : Filter {Power P} {P} (λ x → x) )
-       (ultra : ultra-filter F ) : Set (suc (suc n)) where
-   field
-       limit : Ordinal
-       P∋limit : odef P limit
-       is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ⊆ (* v)
+       u⊆v : * u ⊆ * v
 
 --
 -- Neighbor on x is a Filter (on Power P)
 --
-NeighborF : {P : HOD} (TP : Topology P)  (x : Ordinal ) → Filter {Power P} {P} (λ x → x) 
+NeighborF : {P : HOD} (TP : Topology P)  (x : Ordinal ) → Filter {Power P} {P} (λ x → x)
 NeighborF {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = f1 ; filter2 = f2 } where
     nf00 : {v : Ordinal } → Neighbor TP x v → odef (Power P) v
     nf00 {v} nei y vy = Neighbor.v⊆P nei vy
@@ -480,144 +473,26 @@
     NF⊆PP : NF ⊆ Power P
     NF⊆PP = nf00 
     f1 : {p q : HOD} → Power P ∋ q → NF ∋ p → p ⊆ q → NF ∋ q
-    f1 {p} {q} Pq Np p⊆q = record { u = Neighbor.u Np ; ou = Neighbor.ou Np ; ux = Neighbor.ux Np ; v⊆P = Pq _ ; o⊆u = f11 } where
+    f1 {p} {q} Pq Np p⊆q = record { u = Neighbor.u Np ; ou = Neighbor.ou Np ; ux = Neighbor.ux Np ; v⊆P = Pq _ ; u⊆v = f11 } where
         f11 :  * (Neighbor.u Np) ⊆ * (& q)
-        f11 {x} ux = subst (λ k → odef k x ) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso (Neighbor.o⊆u Np ux)) )
+        f11 {x} ux = subst (λ k → odef k x ) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso (Neighbor.u⊆v Np ux)) )
     f2 : {p q : HOD} → NF ∋ p → NF ∋ q → Power P ∋ (p ∩ q) → NF ∋ (p ∩ q)
-    f2 {p} {q} Np Nq Ppq = record { u = upq ; ou = ou ; ux = ux ; v⊆P = Ppq _ ; o⊆u = f20 } where
+    f2 {p} {q} Np Nq Ppq = record { u = upq ; ou = ou ; ux = ux ; v⊆P = Ppq _ ; u⊆v = f20 } where
          upq : Ordinal
          upq = & ( * (Neighbor.u Np) ∩ * (Neighbor.u Nq) )
          ou : odef (OS TP) upq
          ou = o∩ TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Np)) (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Nq))
          ux :  odef (* upq) x
-         ux = subst ( λ k → odef k x ) (sym *iso) ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫ 
+         ux = subst ( λ k → odef k x ) (sym *iso) ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫
          f20 : * upq ⊆ * (& (p ∩ q))
          f20 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) ( λ {x} pq 
-           → ⟪ subst (λ k → odef k x) *iso (Neighbor.o⊆u Np (proj1 pq))  , subst (λ k → odef k x) *iso (Neighbor.o⊆u Nq (proj2 pq)) ⟫  )
-
--- FIP is UFL
-
--- filter Base
-record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
-   field
-       b x : Ordinal
-       b⊆X : * b ⊆ * X
-       sb  : Subbase (* b) x
-       u⊆P : * u ⊆ P
-       x⊆u : * x ⊆ * u
-
-open import maximum-filter O
+           → ⟪ subst (λ k → odef k x) *iso (Neighbor.u⊆v Np (proj1 pq))  , subst (λ k → odef k x) *iso (Neighbor.u⊆v Nq (proj2 pq)) ⟫  )
 
 CAP : (P : HOD) {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q)
 CAP P {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) *iso pqx
 ... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) (sym *iso) px )
 
-UFLP→FIP : {P : HOD} (TP : Topology P) →
-   ((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
-   -- P is empty
-   fip02 : {x : Ordinal } → ¬ odef P x
-   fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) )
-... | tri> ¬a ¬b 0<P = record { limit = uf00 ; is-limit = uf01 } where
-     fip : {X : Ordinal} → * X ⊆ CS TP → Set n
-     fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
-     N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
-     N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
-        ; <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 = ?
-     0<PP : o∅ o< & (Power P)
-     0<PP = ?
-     F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x)
-     F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where
-         f1 :  {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
-         f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q =
-                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp →
-                            subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp)))  } where
-              f10 : q ⊆ P
-              f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx  ))
-         f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
-         f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where
-              p∩q⊆p : * (& (p ∩ q)) ⊆ P
-              p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx ))
-              Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq)
-              xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq)
-              sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
-              sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
-              f20 : * (& Np+Nq) ⊆ * X
-              f20 {x} npq with subst (λ k → odef k x) *iso npq
-              ... | case1 np = FBase.b⊆X Np np
-              ... | case2 nq = FBase.b⊆X Nq nq
-              f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
-              f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
-                 → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
-     proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅)
-     proper = ?
-     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)
-     ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( MaximumFilter.mf (maxf 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)
-     uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
-     uf00 {X} CSX fp = UFLP.limit ( uflp ( MaximumFilter.mf (maxf CSX fp) ) (ultraf CSX fp))
-     uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
-            {x : Ordinal} → odef (* X) x → odef (* x) (uf00 CSX fip)
-     uf01 {X} CSX fp {x} xx = UFLP.is-limit ( uflp  ( MaximumFilter.mf (maxf CSX fp) ) (ultraf CSX fp)) ? ?
-            
+NEG : (P : HOD) {p : HOD } → Power P ∋ p → Power P ∋ (P ＼ p )
+NEG P {p} Pp x vx with subst (λ k → odef k x) *iso vx
+... | ⟪ Px , npx ⟫ = Px
 
-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
-     CF : HOD
-     CF = Replace' (filter F) (λ x fx → Cl TP x  )
-     CF⊆CS : CF ⊆ CS TP
-     CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) 
-     ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x
-     ufl01 = ?
-     ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) (FIP.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  
-     ufl00 :  {v : Ordinal} → Neighbor TP (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ) v → filter F ⊆ * v
-     ufl00 {v} nei {x} fx = ?
-
--- 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) uflPQ ) where
-     uflP : (F : Filter {Power P} {P} (λ x → x))  (UF : ultra-filter F)
-             → UFLP TP F UF
-     uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF
-     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
-     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
-         FP : Filter {Power P} {P} (λ x → x)
-         FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
-             ty00 :  Proj1 (filter F) (Power P) (Power Q) ⊆ Power P
-             ty00 {x} ⟪ PPx , ppf ⟫ = PPx
-         UFP : ultra-filter FP
-         UFP = record { proper = ? ; ultra = ? }
-         uflp : UFLP TP FP UFP
-         uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
-
-         FQ : Filter {Power Q} {Q} (λ x → x)
-         FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
-             ty00 :  Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q
-             ty00 {x} ⟪ QPx , ppf ⟫ = QPx
-         UFQ : ultra-filter FQ
-         UFQ = record { proper = ? ; ultra = ? }
-         uflq : UFLP TQ FQ UFQ
-         uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ
-
-         Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
-         Pf = ?
-         isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ⊆ * v
-         isL {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } {x} fx = ?
-
diff -r 46dc298bdd77 -r b2ca37e81ad0 src/Tychonoff.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tychonoff.agda	Sun Jan 22 20:04:57 2023 +0900
@@ -0,0 +1,205 @@
+open import Level
+open import Ordinals
+module Tychonoff {n : Level } (O : Ordinals {n})   where
+
+open import zf
+open import logic
+open _∧_
+open _∨_
+open Bool
+
+import OD
+open import Relation.Nullary
+open import Data.Empty
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+import BAlgebra
+open BAlgebra O
+open inOrdinal O
+open OD O
+open OD.OD
+open ODAxiom odAxiom
+import OrdUtil
+import ODUtil
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
+import ODC
+open ODC O
+
+open import filter O
+open import OPair O
+open import Topology O
+open import maximum-filter O
+
+open Filter  
+open Topology 
+
+-- FIP is UFL
+
+-- filter Base
+record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
+   field
+       b x : Ordinal
+       b⊆X : * b ⊆ * X
+       sb  : Subbase (* b) x
+       u⊆P : * u ⊆ P
+       x⊆u : * x ⊆ * u
+
+record UFLP {P : HOD} (TP : Topology P)  (F : Filter {Power P} {P} (λ x → x) )
+       (ultra : ultra-filter F ) : Set (suc (suc n)) where
+   field
+       limit : Ordinal
+       P∋limit : odef P limit
+       is-limit : {v : Ordinal} → Neighbor TP limit v → (* v) ⊆ filter F
+
+UFLP→FIP : {P : HOD} (TP : Topology P) →
+   ((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
+   -- P is empty
+   fip02 : {x : Ordinal } → ¬ odef P x
+   fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) )
+... | tri> ¬a ¬b 0<P = record { limit = limit ; is-limit = uf01 } where
+     fip : {X : Ordinal} → * X ⊆ CS TP → Set n
+     fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
+     N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
+     N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
+        ; <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 = ?
+     0<PP : o∅ o< & (Power P)
+     0<PP = ?
+     F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x)
+     F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where
+         f1 :  {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
+         f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q =
+                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp →
+                            subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp)))  } where
+              f10 : q ⊆ P
+              f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx  ))
+         f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
+         f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where
+              p∩q⊆p : * (& (p ∩ q)) ⊆ P
+              p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx ))
+              Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq)
+              xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq)
+              sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
+              sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
+              f20 : * (& Np+Nq) ⊆ * X
+              f20 {x} npq with subst (λ k → odef k x) *iso npq
+              ... | case1 np = FBase.b⊆X Np np
+              ... | case2 nq = FBase.b⊆X Nq nq
+              f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
+              f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
+                 → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
+     proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅)
+     proper = ?
+     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)
+     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)
+     limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
+     limit {X} CSX fp = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp))
+     uf02 : {X v  : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) 
+        → 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
+     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))
+     ... | yes y = subst (λ k → odef (* x) k) &iso y
+     ... | no nxl = ⊥-elim ( MaximumFilter.proper (maxf CSX fp) uf08 )  where
+         uf03 : OS TP ∋  ( P ＼ (* x))
+         uf03 = ?
+         uf05 : odef ( P ＼ (* x)) (limit CSX fp)
+         uf05 = ⟪  ? , subst (λ k → ¬ odef (* x) k) ?  nxl ⟫
+         uf04 : Neighbor TP (limit CSX fp) (& ( P ＼ (* (limit CSX fp))))
+         uf04 = record { u = & ( P ＼ (* x)) ; ou = ? ; ux = ? ; v⊆P = ? ; u⊆v = ? }
+         uf07 : odef (filter (mf CSX fp)) x
+         uf07 = ?
+         uf06 : odef (filter (mf CSX fp)) (& ( P ＼ (* x)) )
+         uf06 = ?
+         uf08 : (filter (mf CSX fp)) ∋ od∅
+         uf08 = ?
+            
+
+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
+     CF : HOD
+     CF = Replace' (filter F) (λ x fx → Cl TP x  )
+     CF⊆CS : CF ⊆ CS TP
+     CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) 
+     ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x
+     ufl01 = ?
+     limit : Ordinal
+     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  
+     ufl03 : {f v : Ordinal } → odef (filter F) f → Neighbor TP limit v → ¬ ( * f ∩ * v ) =h= od∅ 
+     ufl03 {f} {v} ff nei fv=0 = ?
+     pp :  {v x : Ordinal} → Neighbor TP limit v → odef (* v) x → Power P ∋ (* x)
+     pp {v} {x} nei vx z pz = ?
+     ufl00 :  {v : Ordinal} → Neighbor TP limit v → * v ⊆ filter F 
+     ufl00 {v} nei {x} fx with ultra-filter.ultra UF (pp nei fx) (NEG P (pp nei fx))
+     ... | case1 fv = subst (λ k → odef (filter F) k) &iso fv
+     ... | case2 nfv = ?
+
+-- 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) uflPQ ) where
+     uflP : (F : Filter {Power P} {P} (λ x → x))  (UF : ultra-filter F)
+             → UFLP TP F UF
+     uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF
+     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
+     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
+         FP : Filter {Power P} {P} (λ x → x)
+         FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
+             ty00 :  Proj1 (filter F) (Power P) (Power Q) ⊆ Power P
+             ty00 {x} ⟪ PPx , ppf ⟫ = PPx
+         UFP : ultra-filter FP
+         UFP = record { proper = ? ; ultra = ? }
+         uflp : UFLP TP FP UFP
+         uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
+
+         FQ : Filter {Power Q} {Q} (λ x → x)
+         FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
+             ty00 :  Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q
+             ty00 {x} ⟪ QPx , ppf ⟫ = QPx
+         UFQ : ultra-filter FQ
+         UFQ = record { proper = ? ; ultra = ? }
+         uflq : UFLP TQ FQ UFQ
+         uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ
+
+         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 ? → Neighbor TP q ? → ? ⊆ 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 = ?
+
+
+
+
+
+