# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674259372 -32400
# Node ID cd54ee4982493ffc465827527119563e0adf5eba
# Parent  0a6040d914f87449d51fb5e1e603c5b61d623d38
...

diff -r 0a6040d914f8 -r cd54ee498249 src/Topology.agda
--- a/src/Topology.agda	Sat Jan 21 01:52:19 2023 +0900
+++ b/src/Topology.agda	Sat Jan 21 09:02:52 2023 +0900
@@ -66,6 +66,8 @@
 
 open Topology
 
+-- Closure ( Intersection of Closed Set which include A )
+
 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → HOD
 Cl {L} top A = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) }
   ; odmax = & L ; <odmax = odef∧< }
@@ -75,9 +77,11 @@
         → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x)))
     ; eq← =  λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } )
 
+-- Closure is Closed Set
+
 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → CS top ∋ Cl top A 
 CS∋Cl {L} top A = subst (λ k → CS top ∋ k) (==→o≡ cc00) (P＼OS=CS top UOCl-is-OS)  where
-    OCl : HOD
+    OCl : HOD  -- set of open set which it not contains A 
     OCl = record { od = record { def = λ o → odef (OS top) o ∧ ( A ⊆ (L ＼ * o) ) } ; odmax = & (OS top) ; <odmax = odef∧< }
     OCl⊆OS  : OCl ⊆  OS top 
     OCl⊆OS ox  = proj1 ox
@@ -100,9 +104,9 @@
                    begin  * c ≡⟨ sym ( L＼Lx=x cc08 ) ⟩
                    L ＼ (L ＼ * c) ≡⟨ cong (λ k → L ＼ k ) (sym *iso) ⟩
                    L ＼ * (& (L ＼ * c)) ∎ ) ( ac az ) where open ≡-Reasoning
-                -- ksubst ( λ k → A ⊆ ( L ＼ k )) *iso (subst (λ k → A ⊆ k ) (L＼Lx=x ? ) (ac az) )
         cc03 : {x : Ordinal}  → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) → odef (L ＼ Union OCl) x
         cc03 {x} ⟪ Lx , ccx ⟫ = ⟪ Lx , cc04 ⟫ where
+           -- if x is in Cl A, it is in some c : CS, OCl says it is not , i.e. L ＼ o ∋ x, so it is in (L ＼ Union OCl) x
            cc04 : ¬ odef (Union OCl) x
            cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( subst (λ k → odef k x) *iso cc05) ox  where
                 cc05 : odef (* (& (L ＼ * o))) x
@@ -479,7 +483,13 @@
 
 UFLP→FIP : {P : HOD} (TP : Topology P) →
    ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (UF : ultra-filter F ) → UFLP TP LP F UF ) → FIP TP
-UFLP→FIP {P} TP uflp = record { limit = uf00 ; is-limit = {!!} } where
+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 = {!!} } 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
@@ -534,6 +544,30 @@
      ufl00 :  {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v
      ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ?
 
+FilterProduct  : {P Q LP LQ : HOD } 
+     → (LPP : LP ⊆ Power P) (FP : Filter {LP} LPP)  
+     → (LPQ : LQ ⊆ Power Q) (FQ : Filter {LQ} LPQ)  
+     → Filter {ZFP LP LQ} ?
+FilterProduct  = ?
+
+FilterProj  : {P Q LPQ : HOD } 
+     → ( LPPQ : LPQ ⊆ Power (ZFP P Q))
+     → Filter {LPQ} LPPQ
+     → (Filter {Proj1PP LPQ (Power P) (Power Q)} ?) ∧ (Filter {Proj2PP LPQ (Power P) (Power Q)} ?) 
+FilterProj  = ?
+
+ProuctLimit→ProjLimit  : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  
+     → ( {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ)  (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) LPQ F UF )
+     → ( {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP)  (UF : ultra-filter F) → UFLP TP LP F UF) 
+     ∧ ( {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP)  (UF : ultra-filter F) → UFLP TQ LP F UF) 
+ProuctLimit→ProjLimit  = ?
+
+ProjLimit→ProductLimit  : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  
+     → ( {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP)  (UF : ultra-filter F) → UFLP TP LP F UF) 
+     ∧ ( {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP)  (UF : ultra-filter F) → UFLP TQ LP F UF) 
+     → {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ)  (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) LPQ F UF
+ProjLimit→ProductLimit  = ?
+
 -- 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)