# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673833830 -32400
# Node ID 1966127fc14fbd76396ea61436b47ba8d73275c5
# Parent  f8c3537e68a65373d4ddacde6bc6e12777e46c34
wrong cover definition

diff -r f8c3537e68a6 -r 1966127fc14f src/Topology.agda
--- a/src/Topology.agda	Mon Jan 16 02:22:03 2023 +0900
+++ b/src/Topology.agda	Mon Jan 16 10:50:30 2023 +0900
@@ -241,7 +241,16 @@
 -- FIP is Compact
 
 FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top  → Compact top
-FIP→Compact {L} top fip = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where
+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
+   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 ?
+... | 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
    CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))