--- a/src/Tychonoff.agda	Wed Apr 05 17:05:32 2023 +0900
+++ b/src/Tychonoff.agda	Thu Apr 06 09:16:52 2023 +0900
@@ -35,7 +35,7 @@
 open import filter O
 open import ZProduct O
 open import Topology O
--- open import maximum-filter O
+open import maximum-filter O
 
 open Filter
 open Topology
@@ -80,6 +80,15 @@
        P∋limit : odef P limit
        is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v)
 
+--
+-- If Any ultra filter has a limit that is  all neighbor of the limit is in the filter,
+-- it has finite intersection property.
+--
+-- Finite intersection defines a filter, so we have a ultra filter becaause Zorn lemma maximizing it.
+-- If the limit of filter is not contained by a closed set p in FIP, it is in P \ p. It is open and
+-- contains the limit, so it is in the ultra filter. This means p and P \ p is in the filter, which
+-- contradicts proper of the ultra filter.
+--
 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∅
@@ -176,13 +185,13 @@
      --    otherwise the check requires a minute
      --
      maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
-     maxf {X} 0<X CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
      mf {X} 0<X CSX fp =  MaximumFilter.mf (maxf 0<X CSX fp)
      ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
-     ultraf {X} 0<X CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      --
-     -- so it has a limit as a limit of UIP
+     -- so it has a limit as a limit of FIP
      --
      limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
      limit {X} CSX fp with trio< o∅ X
@@ -243,6 +252,13 @@
 P⊆Clx : {P : HOD} (TP : Topology P) →  {x : HOD} → x ⊆ P   → Cl TP x ⊆ P
 P⊆Clx {P} TP {x}  x<p {y} xy  = proj1 xy
 
+--
+-- Finite intersection property implies that any ultra filter have a limit, that is, neighbors of the limit is in the filter.
+--
+-- An ultra filter F is given. Take a closure of a filter. It is closed and it has finite intersection property, because F is porper.
+-- So it has a limit as a FIP. If a neighbor p which contains the limit, p or P \ p is in the ultra filter.
+-- If it is in P \ p, it cannot contains the limit, contradiction.
+--
 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
@@ -345,18 +361,24 @@
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
-FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
-     → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) 
-FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } 
+--    FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
+--         → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) 
+--    FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } 
+-- 
+--    projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
+--         → Filter {Power P} {P} (λ x → x) 
+--    projection-of-filter = ?
+-- 
+--    projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F) 
+--         → ultra-filter (projection-of-filter F)
+--    projection-of-ultra-filter = ?
 
-projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
-     → Filter {Power P} {P} (λ x → x) 
-projection-of-filter = ?
-
-projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F) 
-     → ultra-filter (projection-of-filter F)
-projection-of-ultra-filter = ?
-
+--
+-- We have UFLP both in P and Q. Given an ultra filter F on P x Q. It has limits on P and Q because a projection of ultra filter
+-- is a ultra filter. Show the product of the limits is a limit of P x Q. A neighbor of P x Q contains subbase of P x Q,
+-- which is either inverse projection x of P or Q. The x in in projection of F, because of UFLP. So it is in F, because of the
+-- property of the filter.
+--
 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)