--- a/src/Topology.agda	Mon Dec 26 14:00:57 2022 +0900
+++ b/src/Topology.agda	Wed Dec 28 18:14:29 2022 +0900
@@ -31,6 +31,8 @@
 open ODC O
 
 open import filter
+open import OPair O
+
 
 record Topology  ( L : HOD ) : Set (suc n) where
    field
@@ -38,9 +40,16 @@
        OS⊆PL :  OS ⊆ Power L 
        o∪ : { P : HOD }  →  P  ⊆ OS           → OS ∋ Union P
        o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q  → OS ∋ (p ∩ q)
+-- closed Set
+   CS : HOD
+   CS = record { od = record { def = λ x → odef OS (& ( L ＼ (* x ))) } ; odmax = & L ; <odmax = tp02 } where
+       tp02 : {y : Ordinal } → odef OS (& (L ＼ * y)) → y o< & L
+       tp02 {y} nop = ?
+       -- ∈∅< ( proj1 nop )
 
 open Topology
 
+
 record _covers_ ( P q : HOD  ) : Set (suc n) where
    field
        cover   : {x : HOD} → q ∋ x → HOD
@@ -58,7 +67,7 @@
 
 -- Limit point
 
-record LP ( L S x : HOD ) (top : Topology L) (S⊆PL :  S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where
+record LP { L : HOD}  (top : Topology L) ( S x : HOD ) (S⊆PL :  S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where
    field
       neip   : {y : HOD} → OS top ∋ y → y ∋ x → HOD
       isNeip : {y : HOD} → (o∋y : OS top ∋ y ) → (y∋x : y ∋ x ) → ¬ ( x ≡ neip o∋y y∋x) ∧ ( y ∋ neip o∋y y∋x )
@@ -66,38 +75,49 @@
 -- Finite Intersection Property
 
 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
-   fin-∩e : {x : HOD} → S ∋ x → Finite-∩ S x
-   fin-∩  : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
+   fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
+   fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
 
-record FIP  ( L P : HOD ) : Set (suc n) where
+record FIP {L : HOD} (top : Topology L)  ( P : HOD ) : Set (suc n) where
    field
-       fipS⊆PL :  P ⊆ Power L 
+       fipS⊆PL :  P ⊆ CS top
        fip≠φ : { x : HOD } → Finite-∩ P x → ¬ ( x ≡ od∅ )
 
 -- Compact
 
 data Finite-∪ (S : HOD) : HOD → Set (suc n) where
-   fin-∪e : {x : HOD} → S ∋ x → Finite-∪ S x
+   fin-e : {x : HOD} → S ∋ x → Finite-∪ S x
    fin-∪  : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
 
-record Compact  ( L P : HOD ) : Set (suc n) where
+record Compact  {L : HOD} (top : Topology L) ( P : HOD ) : Set (suc n) where
    field
-       finCover        : {X y : HOD} → X covers P         → P ∋ y →  HOD
-       isFinCover      : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → finCover xp P∋y ∋ y
-       isFininiteCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → Finite-∪ X (finCover xp P∋y )
+       finCover        : {X : HOD} → X ⊆ OS top → X covers P → HOD
+       isFinCover      : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → (finCover xo xcp ) covers P
+       isFiniteCover   : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → Finite-∪ X (finCover xo xcp  )
 
 -- FIP is Compact
 
-FIP→Compact : {L P : HOD} → Topology L → FIP L P → Compact L P
-FIP→Compact = {!!}
+FIP→Compact : {L P : HOD} → (top : Topology L ) → FIP top P → Compact top P
+FIP→Compact {L} {P} TL fip = record { finCover = ? ; isFinCover = ? ; isFiniteCover = ? }
 
-Compact→FIP : {L P : HOD} → Topology L → Compact L P → FIP L P
+Compact→FIP : {L P : HOD} → (top : Topology L ) → Compact top P → FIP top P
 Compact→FIP = {!!}
 
 -- Product Topology
 
-_Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology {!!}
-_Top⊗_ = {!!}
+open ZFProduct 
+
+_Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
+_Top⊗_ {P} {Q} TP TQ = record {
+       OS    = POS
+    ;  OS⊆PL = ?
+    ;  o∪ = ?
+    ;  o∩ = ?
+  } where
+      box : HOD
+      box = ZFP (OS TP) (OS TQ) 
+      POS : HOD
+      POS = ?
 
 -- existence of Ultra Filter