--- a/Topology.agda	Sat Dec 19 21:43:21 2020 +0900
+++ b/Topology.agda	Sat Dec 19 21:58:32 2020 +0900
@@ -69,23 +69,41 @@
    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
+   field
+       fipS⊆PL :  P ⊆ Power L 
+       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-∪  : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
 
-record FIP  ( L : HOD ) : Set (suc n) where
-   field
-       fipS     : HOD
-       fipS⊆PL :  fipS ⊆ Power L 
-       fip≠φ : { x : HOD } → Finite-∩ fipS x → ¬ ( x ≡ od∅ )
-
--- Compact
-
 record Compact  ( 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 )
 
+-- FIP is Compact
+
+FIP→Compact : {L P : HOD} → Tolopogy L → FIP L P → Compact L P
+FIP→Compact = ?
+
+Compact→FIP : {L P : HOD} → Tolopogy L → Compact L P → FIP L P
+Compact→FIP = ?
 
 -- Product Topology
+
+_Top⊗_ : {P Q : HOD} → Topology P → Tolopogy Q → Topology ( P ⊗ Q )
+_Top⊗_ = ?
+
+-- existence of Ultra Filter 
+
+-- Ultra Filter has limit point
+
+-- FIP is UFL
+
+-- Product of UFL has limit point (Tychonoff)
+