# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673841291 -32400
# Node ID 607a79aef2978779ac754f43b14b521c9896039a
# Parent  1966127fc14fbd76396ea61436b47ba8d73275c5
Union for cover

diff -r 1966127fc14f -r 607a79aef297 src/OD.agda
--- a/src/OD.agda	Mon Jan 16 10:50:30 2023 +0900
+++ b/src/OD.agda	Mon Jan 16 12:54:51 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 607a79aef297 src/Topology.agda
--- a/src/Topology.agda	Mon Jan 16 10:50:30 2023 +0900
+++ b/src/Topology.agda	Mon Jan 16 12:54:51 2023 +0900
@@ -203,13 +203,8 @@
 
 -- covers
 
-record _covers_ ( P q : HOD  ) : Set n where
-   field
-       cover   : {x : Ordinal } → odef q x → Ordinal
-       P∋cover : {x : Ordinal } → (lt : odef q  x) → odef P (cover lt)
-       isCover : {x : Ordinal } → (lt : odef q  x) → odef (* (cover lt))  x
-
-open _covers_
+_covers_ : ( P q : HOD  ) →  Set n 
+P covers q = q ⊆ Union P
 
 -- Finite Intersection Property
 
@@ -243,13 +238,13 @@
 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 = λ {X} xo xcp → ? ; isCover = λ {X} _ xcp → fip01 xcp ; isFinite = fip00 }  where
    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 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 ?
+   fip01 : {X : Ordinal } → (xcp : * X covers L) → * ? covers L
+   fip01 xcp = ?
+   fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) ?
+   fip00 {X} xo xcp = fin-e ?  
 ... | 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
@@ -308,7 +303,7 @@
               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 _ ))
+          fip09 {z} Lz nc  =  nc ? (subst (λ k → odef ? k) refl ?)
    ¬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)