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

diff -r 1966127fc14f -r d39c79bb71f0 src/OD.agda
--- a/src/OD.agda	Mon Jan 16 10:50:30 2023 +0900
+++ b/src/OD.agda	Mon Jan 16 14:01:45 2023 +0900
@@ -217,6 +217,9 @@
 ∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
 ∅<  {x} {y} d eq | lift ()
 
+0<P→ne  : { x : HOD  } → o∅ o< & x → ¬ (  od x  == od od∅  )
+0<P→ne {x} 0<x eq = ⊥-elim ( o<¬≡ (sym (=od∅→≡o∅ eq)) 0<x )
+
 ∈∅< : { x : HOD  } {y : Ordinal } → odef x y → o∅  o< (& x)
 ∈∅<  {x} {y} d with trio< o∅ (& x)
 ... | tri< a ¬b ¬c = a
diff -r 1966127fc14f -r d39c79bb71f0 src/Topology.agda
--- a/src/Topology.agda	Mon Jan 16 10:50:30 2023 +0900
+++ b/src/Topology.agda	Mon Jan 16 14:01:45 2023 +0900
@@ -229,7 +229,7 @@
 -- Compact
 
 data Finite-∪ (S : HOD) : Ordinal → Set n where
-   fin-e : {x : Ordinal } → odef S x → Finite-∪ S x
+   fin-e : {x : Ordinal } → * x ⊆ S → 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
@@ -243,13 +243,14 @@
 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top  → Compact top
 FIP→Compact {L} top fip with trio< (& L) o∅ 
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-... | tri≈ ¬a b ¬c = record { finCover = λ _ _ → & ( od∅ , od∅ ) ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 }  where
+... | tri≈ ¬a b ¬c = record { finCover = λ _ _ → o∅ ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 }  where
+   -- L is empty
    fip02 : {x : Ordinal } → ¬ odef L x
    fip02 {x} Lx = ⊥-elim ( o<¬≡ (sym b) (∈∅< Lx) )
-   fip01 : {X : Ordinal } → (xcp : * X covers L) → * (& ( od∅ , od∅ )) covers L
+   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) (& ( od∅ , od∅ ))
-   fip00 {X} xo xcp = fin-e ?
+   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) ) )
 ... | 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
@@ -270,9 +271,6 @@
       fip06 = os ( subst (λ k → odef (* X) k ) fip07 az )
       fip05 : * x ⊆ L
       fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw )
-   -- 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 
    --
    --   X covres L means Intersection of (CX X) contains nothing
    --     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP )
@@ -281,44 +279,46 @@
    record CFIP (x : Ordinal) : Set n where
       field
          is-CS : * x ⊆ CS top
-         y : Ordinal 
-         sy :  Subbase (* y)  o∅ 
+         sx :  Subbase (* x)  o∅ 
    Cex : HOD
    Cex = record { od = record { def = λ x → CFIP x } ; odmax = osuc (& (CS top)) ; <odmax = λ {x} lt → 
         subst₂ (λ j k → j o≤ k ) &iso refl ( ⊆→o≤ (CFIP.is-CS lt )) }
+   fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex  =h= od∅ ) 
+   fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where 
+       -- CX is finite intersection
+       fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
+       fip02 {C} {x} C<CX 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 (* C) k) b sc } )) where
+           fip10 : * C ⊆  CS top
+           fip10 {w} cw = CCX ox ( C<CX cw )
+       -- we have some intersection because L is not empty
+       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)  
+          record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L))  ; x=ψz = refl } 
+       fip25 : odef L( FIP.limit fip (CCX ox) fip02 )
+       fip25 = FIP.L∋limit fip (CCX ox) fip02 fip26
+       fip20 : {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 ))
+       fip20 {y} Xy yl = proj2 fip21 yl where
+           fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
+           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  fip00)  where
-      fip00 : ¬ ( Cex  =h= od∅ ) 
-      fip00 cex=0 = ⊥-elim (fip09 fip25 fip20) 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 {C} {x} C<CX 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 ; y = C ; sy = subst (λ k → Subbase (* C) k) b sc } )) where
-              fip10 : * C ⊆  CS top
-              fip10 {w} cw = CCX ox ( C<CX cw )
-          fip25 : odef L( FIP.limit fip (CCX ox) fip02 )
-          fip25 = FIP.L∋limit fip (CCX ox) fip02 ?
-          fip20 : {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 ))
-          fip20 {y} Xy yl = proj2 fip21 yl where
-              fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
-              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 _ ))
-   ¬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 (cex ox oc)
-      fip04 = {!!}
+   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)
    -- 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 = {!!}
+   isFinite {X} xo xcp = {!!} where
+        fip30 : {y z : Ordinal } →  Subbase (* y)  o∅  → Finite-∪ (* X) z
+        fip30 = ?
    -- is also a cover
    isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
    isCover1 = {!!}