--- a/src/Topology.agda	Mon Jan 02 10:15:20 2023 +0900
+++ b/src/Topology.agda	Tue Jan 03 09:28:23 2023 +0900
@@ -141,17 +141,23 @@
 
 -- covers
 
-record _covers_ ( P q : HOD  ) : Set (suc n) where
+record _covers_ ( P q : HOD  ) : Set n where
    field
-       cover   : {x : HOD} → q ∋ x → HOD
-       P∋cover : {x : HOD} → {lt : q ∋ x} → P ∋ cover lt
-       isCover : {x : HOD} → {lt : q ∋ x} → cover lt ∋ x
+       cover   : {x : Ordinal } → odef q x → Ordinal
+       P∋cover : {x : Ordinal } → {lt : odef q  x} → odef P (cover lt)
+       isCover : {x : Ordinal } → {lt : odef q  x} → odef (* (cover lt))  x
+
+open _covers_
 
 -- Finite Intersection Property
 
-record FIP {L : HOD} (top : Topology L) : Set (suc n) where
+record FIP {L : HOD} (top : Topology L) : Set n where
    field
-       fip≠φ : { C : HOD } { x : Ordinal } → C ⊆ CS top → Subbase C x → o∅ o< x 
+       finite : {X : Ordinal } → * X ⊆ CS top 
+          →       ( { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  Ordinal
+       limit : {X : Ordinal } → (CX : * X ⊆ CS top )
+          → ( fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) 
+          →  {x : Ordinal } → odef (* X) x → odef (* x) (finite CX fip)
 
 -- Compact
 
@@ -159,20 +165,36 @@
    fin-e : {x : Ordinal } → odef S x → Finite-∪ S x
    fin-∪  : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
 
-record Compact  {L : HOD} (top : Topology L)  : Set (suc n) where
+record Compact  {L : HOD} (top : Topology L)  : Set n where
    field
-       finCover  : {X : HOD} → X ⊆ OS top → X covers L → HOD
-       isCover   : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L
-       isFinite  : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (& (finCover xo xcp  ) )
+       finCover  : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal
+       isCover   : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L
+       isFinite  : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → Finite-∪ (* X) (finCover xo xcp ) 
 
 -- FIP is Compact
 
 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top  → Compact top
-FIP→Compact {L} top fip = record { finCover = finCover ; isCover = ? ; isFinite = ? } where
-    finCover  : {C : HOD} → C ⊆ OS top → C covers L → HOD
-    finCover {C} C<T CL = record { od = record { def = λ x → odef L x ∧ ( ¬ Subbase C x) } ; odmax = & L ; <odmax = odef∧< }
-    isConver : {C : HOD} (xo : C ⊆ OS top) (xcp : C covers L) → (finCover xo xcp) covers L
-    isConver {C} xo xcp = record { cover = λ lx → ? ; P∋cover = ? ; isCover = ? }
+FIP→Compact {L} top fip = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where
+   remain : {X : Ordinal } → (* X) ⊆ OS top → ¬ ( (* X) covers L ) → Ordinal 
+   remain = ?
+   remain-is-intersection : {X : Ordinal } → (ox : (* X) ⊆ OS top) → (r : ¬ ( (* X) covers L ) )
+       →  {x : Ordinal } → odef (* X) x → odef (L ＼ * x ) (remain ox r)
+   -- HOD of a counter example of fip 
+   tp00 : {X : Ordinal} → * X ⊆ OS top → HOD
+   tp00 {X} ox = record { od = record { def = λ x → { C : Ordinal  } → * C ⊆ * X → Subbase (L ＼ * C) x }
+       ; odmax = & L ; <odmax = ? }
+   finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
+   finCover {X} ox oc = ? where
+        -- X is the counter example of fip
+        tp01 : {x : Ordinal } → odef (L ＼  * X) ( FIP.finite fip ? ?  ) → odef (* x) ( FIP.finite fip ? ?  )
+        tp01 {x} P = FIP.limit fip ? ? ? 
+   -- yes, it is finite
+   isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
+   isFinite = ?
+   -- is also a cover
+   isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
+   isCover1 = ?
+
 
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
 Compact→FIP = {!!}