# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677403823 -32400
# Node ID 0201827b08ac8aaefc32cafcb0a7f0f1d60f3976
# Parent  8cbc3918d875342ff23b71220ecbba3d6ccc2fa9
...

diff -r 8cbc3918d875 -r 0201827b08ac src/Topology.agda
--- a/src/Topology.agda	Sun Feb 26 11:16:32 2023 +0900
+++ b/src/Topology.agda	Sun Feb 26 18:30:23 2023 +0900
@@ -281,7 +281,7 @@
 
 data Finite-∪ (S : HOD) : Ordinal → Set n where
    fin-e : Finite-∪ S o∅
-   fin-i : {x : Ordinal } → * x ⊆ S → Finite-∪ S x
+   fin-i : {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
@@ -328,24 +328,18 @@
    --     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP)
    --     it means there is a finite cover
    --
-   record CFIP (X x : Ordinal) : Set n where
-      field
-         is-CS : * x ⊆ Replace (* X) (λ z → L ＼ z)
-         sx :  Subbase (* x)  o∅
-   Cex : (X : Ordinal ) → HOD
-   Cex X = record { od = record { def = λ x → CFIP X x } ; odmax = osuc (& (Replace (* X) (λ z → L ＼ z))) ; <odmax = fip05 } where
-       fip05 :  {y : Ordinal} →   CFIP X y → y o< osuc (& (Replace (* X) (λ z → L ＼ z)))
-       fip05 {y} cf = subst₂ (λ j k → j o< osuc k ) &iso refl ( ⊆→o≤ ( CFIP.is-CS cf ) )
-   fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex X =h= od∅ )
-   fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where
+   finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L →  Subbase (Replace (* X) (λ z → L ＼ z)) o∅
+   finCoverBase {X} ox oc with ODC.p∨¬p O (Subbase (Replace (* X) (λ z → L ＼ z)) o∅)
+   ... | case1 sb = sb
+   ... | case2 ¬sb = ⊥-elim (fip09 fip25 fip20) where
+       fip09 : {z : Ordinal } →  odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) z ))
+       fip09 {z} Lz nc  =  nc ( P∋cover oc Lz  ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
        -- CX is finite intersection
        fip02 : {x : Ordinal} → Subbase (* (CX ox)) x → o∅ o< x
        fip02 {x} sc with trio< x o∅
        ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
        ... | tri> ¬a ¬b c = c
-       ... | tri≈ ¬a b ¬c  = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; sx = subst (λ k → Subbase (* (CX ox)) k) b sc } )) where
-           fip10 : * (CX ox) ⊆ Replace (* X) (λ z → L ＼ z)
-           fip10 {w} cw = subst (λ k → odef k w) *iso cw 
+       ... | tri≈ ¬a b ¬c  = ⊥-elim (¬sb (subst₂ (λ j k → Subbase j k ) *iso b sc )) 
        -- we have some intersection because L is not empty (if we have an element of L, we don't need choice)
        fip26 : odef (* (CX ox))    (& (L ＼  * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )))
        fip26 = subst (λ k → odef k (& (L ＼  * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso)
@@ -358,53 +352,37 @@
            fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl }
            fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 )
            fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 )
-       fip09 : {z : Ordinal } →  odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) z ))
-       fip09 {z} Lz nc  =  nc ( P∋cover oc Lz  ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
-   cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
-   cex {X} ox oc = & ( ODC.minimal O (Cex X) (fip00 ox oc))   -- this will be the finite cover
-   CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → CFIP X (cex ox oc)
-   CXfip {X} ox oc  = ODC.x∋minimal O (Cex X) (fip00 ox oc)
+   finCoverSet : {X : Ordinal } → (x : Ordinal) →  Subbase (Replace (* X) (λ z → L ＼ z)) x → HOD
+   finCoverSet {X} x (gi rx) = L ＼ * x 
+   finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy 
    --
    -- this defines finite cover
    finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
-   finCover {X} ox oc = & ( Replace (* (cex ox oc)) (λ z → L ＼  z ))
+   finCover {X} ox oc = & ( finCoverSet o∅ (finCoverBase ox oc))
    -- create Finite-∪ from cex
    isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
-   isFinite {X} xo xcp = fip30 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp)) where
-        fip30 : ( x y : Ordinal ) → * x ⊆ Replace (* X) (λ z → L ＼ z) →  Subbase (* x) y → Finite-∪ (* X) (& (Replace (* x) (λ z → L ＼  z )))
-        fip30 x y x⊆cs (gi sb) = fip31 where
-            fip32 : Replace (* x) (λ z → L ＼ z) ⊆ * X 
-            fip32 {w} record { z = z ; az = xz ; x=ψz = x=ψz } with x⊆cs xz
-            ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
+   isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where
+        fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb))
+        fip60 x (gi rx) = fin-i (fip61 rx) where
+           fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) ))
+           fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
                fip34 : * z1 ⊆ L
                fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1
-               fip33 : z1 ≡ w
+               fip33 : z1 ≡ & (L ＼ * x)
                fip33 = begin
                  z1 ≡⟨ sym &iso ⟩
                  & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩
                  & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
                  & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
-                 & (L ＼ * z) ≡⟨ sym x=ψz ⟩
-                 w ∎ where open ≡-Reasoning
-            --  x⊆cs :* x ⊆ Replace (* X) (λ z₁ xz → L ＼ z₁) , x=ψz : w ≡ & (L ＼ * z) , odef (* x) z
-            fp38 : Subbase (* x) y 
-            fp38 = gi sb
-            fp35 : odef (* x) y
-            fp35 = sb
-            fp36 : odef (Replace (* X) (λ z → L ＼ z)) y
-            fp36 = x⊆cs sb
-            fp37 : odef (* X) (& (L ＼ * y))
-            fp37 = ?
-            fip31 : Finite-∪ (* X) (& (Replace (* x) (λ z → L ＼ z)))
-            fip31 = fin-i (subst (λ k → k ⊆ * X ) (sym *iso) fip32 )
-        fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = fip35 where
-            fip35 : Finite-∪ (* X) (& (Replace (* x) (λ z₁ → L ＼ z₁)))
-            fip35 = subst (λ k → Finite-∪ (* X) k)
-               (cong (&) (subst (λ k → (k ∪ k ) ≡ (Replace (* x) (λ z₁ → L ＼ z₁)) ) (sym *iso) x∪x≡x )) ( fin-∪ (fip30 _ _  x⊆cs sy)  (fip30 _ _ x⊆cs sz) )
+                 & (L ＼ * x ) ∎ where open ≡-Reasoning
+        fip60 x∩y (g∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx)  (fip60 y sy)  ) where
+               fip62 : & (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡ & (finCoverSet x sx ∪ finCoverSet y sy)
+               fip62 = cong (&) ( begin
+                  (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ *iso *iso ⟩ 
+                  finCoverSet x sx ∪ finCoverSet y sy ∎ ) where open ≡-Reasoning
    -- is also a cover
    isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
-   isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L)
-     ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where
+   isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L) ? where
         fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪  (L ＼ b))
         fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x)
         ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ )  ⟫