# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673876589 -32400
# Node ID f8a30e568ecaacb384ab05427f22daa3af0196c5
# Parent  d39c79bb71f0009870c7d367ed87c7e505fd5b94
...

diff -r d39c79bb71f0 -r f8a30e568eca src/Topology.agda
--- a/src/Topology.agda	Mon Jan 16 14:01:45 2023 +0900
+++ b/src/Topology.agda	Mon Jan 16 22:43:09 2023 +0900
@@ -229,7 +229,8 @@
 -- Compact
 
 data Finite-∪ (S : HOD) : Ordinal → Set n where
-   fin-e : {x : Ordinal } → * x ⊆ S → Finite-∪ S x
+   fin-∅ : Finite-∪ S o∅
+   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 n where
@@ -250,7 +251,7 @@
    fip01 : {X : Ordinal } → (xcp : * X covers L) → (* o∅) covers L
    fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx)  ; P∋cover = λ Lx → ⊥-elim (fip02 Lx)  ; isCover =  λ Lx → ⊥-elim (fip02 Lx) }
    fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) o∅
-   fip00 {X} xo xcp = fin-e ( λ {x} 0x → ⊥-elim (¬x<0 (subst (λ k → odef k x) o∅≡od∅ 0x) ) )
+   fip00 {X} xo xcp = fin-∅ 
 ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where
    -- set of coset of X
    CX : {X : Ordinal} → * X ⊆ OS top → Ordinal
@@ -311,13 +312,28 @@
    cex {X} ox oc = & ( ODC.minimal O Cex  (fip00 ox oc))  
    CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → CFIP (cex ox oc)
    CXfip {X} ox oc  = ODC.x∋minimal O Cex (fip00 ox oc)
+   -- 
+   --  Subbase (* CCX) s    -- Finite-∪ (* X) (replaced s)
+   --     sa ∩ sb  ≡ s       ( L ＼ sa ) ∪ (L ＼ sb) ≡ (replaced s)
+   --     CCX ∋ s            (replaced s) ∋ ( L ＼ s )   
+   --
+   --  Subbase (* (cex ox oc)) s   -- Finite-∪ (* X) (finCover xo xcp)
+   --     sa ∩ sb                        ( L ＼ sa ) ∪ (L ＼ sb)
+   record Cover+Int {X : Ordinal } (ox : * X ⊆ OS top) (oc : * X covers L) : Set n where
+      field
+         x w : Ordinal
+         is-CS : * x ⊆ CS top
+         x+w=L : (* x ∪ * w ) =h= L
+         sx :  Subbase (* (cex ox oc)) w 
+         fc :  Finite-∪ (* X) x
+   -- 
    -- this defines finite cover
    finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
    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 {X} xo xcp = {!!} where
-        fip30 : {y z : Ordinal } →  Subbase (* y)  o∅  → Finite-∪ (* X) z
+   isFinite {X} xo xcp = ? where
+        fip30 : ( x y : Ordinal ) → * x ⊆ CS top →  Subbase (* x) y → Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼  z )))
         fip30 = ?
    -- is also a cover
    isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L