--- a/src/Topology.agda	Sat Feb 18 11:51:22 2023 +0900
+++ b/src/Topology.agda	Tue Feb 21 12:02:41 2023 +0900
@@ -447,7 +447,38 @@
             fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
 
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
-Compact→FIP = ?
+Compact→FIP {L} top fip with trio< (& L) o∅
+... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
+... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? } 
+... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
+   -- set of coset of X
+   OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
+   OX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
+   OOX : {X : Ordinal} → (cs :  * X ⊆ CS top) → * (OX cs) ⊆ OS top
+   OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox
+   ... | record { z = z ; az = az ; x=ψz = x=ψz } =  subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01))  where
+       comp01 : odef (* X) (& (* z))
+       comp01 = subst (λ k → odef (* X) k) (sym &iso) az
+   --
+   --   if all finite intersection of (OX X) contains something, 
+   --   there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
+   --     it means there is a limit
+   --
+   Intersection : (X : Ordinal ) →  HOD
+   Intersection X = record { od = record { def = λ x → {y : Ordinal} → odef (* X) y → odef (* y) x } ; odmax = ? ; <odmax = ? }
+   has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
+      →  ¬ (  Intersection X  =h= od∅ )
+   has-intersection {X} CX fip i=0 = ? where
+       no-cover : ¬ ( (* (OX CX)) covers L ) 
+       no-cover = ?
+   limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
+      → Ordinal
+   limit = ?
+   fip00 : {X : Ordinal} (CX : * X ⊆ CS top)
+            (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
+            {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip )
+   fip00 = ?
+
 
 open Filter