# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1672723073 -32400
# Node ID 98af35c9711fd63819f99684c0fb22dd28a80b09
# Parent  e086a266c6b75debb1cec938da5f41f600d9af97
...

diff -r e086a266c6b7 -r 98af35c9711f src/Topology.agda
--- a/src/Topology.agda	Tue Jan 03 09:28:23 2023 +0900
+++ b/src/Topology.agda	Tue Jan 03 14:17:53 2023 +0900
@@ -175,20 +175,36 @@
 
 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top  → Compact top
 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 = ? }
+   -- set of coset of X
+   CX : {X : Ordinal} → * X ⊆ OS top → Ordinal
+   CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
+   CCX : {X : Ordinal} → (os :  * X ⊆ OS top) → * (CX os) ⊆ CS top 
+   CCX {X} ox = ?
+   -- CX has finite intersection
+   CXfip : {X : Ordinal } → * X ⊆ OS top → Set n
+   CXfip {X} ox =  { x C : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x 
+   Cex : {X : Ordinal } → * X ⊆ OS top → HOD
+   Cex {X} ox =  record { od = record { def = λ C → { x : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) o∅ } 
+       ; odmax = osuc ( & (Power L)) ; <odmax = ? }
+   -- a counter example of fip , some CX has no finite intersection
+   cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
+   cex {X} ox oc = & ( ODC.minimal O (Cex ox) fip00)  where
+      fip00 : ¬ ( Cex ox =h= od∅ ) 
+      fip00 cex=0 = fip03 ? ? where 
+          fip03 : {x z : Ordinal } → odef (* x) z →  (¬ odef (* x) z) → ⊥
+          fip03 {x} {z} xz nxz = nxz xz
+          fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
+          fip02 = ?
+          fip01 : Ordinal
+          fip01 = FIP.finite fip (CCX ox) fip02
+   ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ 
+   ¬CXfip {X} ox oc = ? where
+      fip04 : odef (Cex ox) (cex ox oc)
+      fip04 = ?
+   -- this defines finite cover
    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
+   finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L ＼  z ))
+   -- create Finite-∪ from cex
    isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
    isFinite = ?
    -- is also a cover