# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677578758 -32400
# Node ID 68239d102d1525c83e723f6b736f138b689b9583
# Parent  6174001ba1c0b9318e72741599d15ced78e1ae7d
...

diff -r 6174001ba1c0 -r 68239d102d15 src/Topology.agda
--- a/src/Topology.agda	Tue Feb 28 15:01:17 2023 +0900
+++ b/src/Topology.agda	Tue Feb 28 19:05:58 2023 +0900
@@ -441,25 +441,20 @@
       fp08 : odef (* X) (& fp07)
       fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
       no-cover : ¬ ( (* (OX CX)) covers L ) 
-      no-cover cov = ⊥-elim ( SB.¬i⊆Ut (fp02 fp01 (Compact.isFinite compact (OOX CX) cov) ) fp12 ) where
+      no-cover cov = ⊥-elim ? where
           fp01 : Ordinal
           fp01 = Compact.finCover compact (OOX CX) cov
           record SB (t : Ordinal) : Set n where
             field
                i : Ordinal 
-               ¬i⊆Ut : ¬ ( (L ＼ * i) ⊆ Union (* t))
                sb : Subbase (* X) (& (L ＼ * i))
           fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t
-          fp02 t fin-e = record { i = & ( L  ＼ fp07) ; ¬i⊆Ut = fp20 ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) } where  
+          fp02 t fin-e = record { i = & ( L  ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) } where  
               fp22 : fp07 ⊆ L
               fp22 {x} lt =  cs⊆L top (CX fp08) lt 
               fp21 : & fp07 ≡ & (L ＼ * (& (L ＼ fp07)))
               fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼  k) (sym *iso)))
-              fp20 : ¬ (L ＼ * (& (L ＼ fp07))) ⊆ Union (* o∅)
-              fp20 lt = ?
-          fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; ¬i⊆Ut = fp23 } where
-              fp23 :  ¬ (L ＼ * x) ⊆ Union (* (& (* x , * x)))
-              fp23 = ?
+          fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 } where
               fp03 :  odef (* X) (& (L ＼ * x))
               fp03 with subst (λ k → odef k x ) *iso tx
               ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
@@ -472,7 +467,7 @@
                      & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
                      & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
                      & (L ＼ * x ) ∎ where open ≡-Reasoning
-          fp02 t (fin-∪ {tx} {ty} x y ) =  record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 ; ¬i⊆Ut = ? } where
+          fp02 t (fin-∪ {tx} {ty} x y ) =  record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11 } where
               fp04 :  {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
               fp04 {tx} {ty} = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where
                   fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x
@@ -488,9 +483,7 @@
               fp11 : Subbase (* X) (& (L ＼ * (& ((* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y)))))))
               fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx x)) (SB.sb (fp02 ty y )) ) 
           fp12 : (L ＼ * (SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov)))) ⊆ Union (* fp01)
-          fp12 {x} ⟪ Lx , not ⟫ = ⊥-elim ( fp14 (λ {y} lt → record { owner = cover fcov (fp16 lt)
-                  ; ao = P∋cover fcov (fp16 lt)
-                  ; ox = isCover fcov (fp16 lt) } ))  where
+          fp12 {x} ⟪ Lx , not ⟫ = fp17 fp19 where
               fcov = Compact.isCover compact (OOX CX) cov
               fp13 : Ordinal 
               fp13 = SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov))
@@ -498,8 +491,18 @@
               fp16 {y} ⟪ Ly , _ ⟫ = Ly
               fp15 : ¬ ( odef (* fp13) x)
               fp15 = not
-              fp14 : ¬ ( (L ＼ * fp13 ) ⊆ Union (* fp01 )) 
-              fp14 = SB.¬i⊆Ut (fp02 fp01 (Compact.isFinite compact (OOX CX) cov))
+              fp19 : odef (L ＼ * fp13) x
+              fp19 with ∨L＼X {L} {* fp13} Lx 
+              fp19 | case1 lt = ⊥-elim (not lt)
+              fp19 | case2 lt = lt
+              fp17 :  (L ＼ * fp13 ) ⊆ Union (* fp01 )
+              fp17 {y} lt = record { owner = cover fcov (fp16 lt) ; ao = P∋cover fcov (fp16 lt) ; ox = isCover fcov (fp16 lt) } 
+          fcov : Finite-∪ (* (OX CX)) (Compact.finCover compact (OOX CX) cov)
+          fcov = Compact.isFinite compact (OOX CX) cov
+          ¬i⊆Ut : {i : Ordinal } → (sb : Subbase (* X) (& (L ＼ * i))) → ¬ ( (L ＼ * i) =h= od∅ )
+          ¬i⊆Ut {i} sb = 0<P→ne (fip sb)
+          f20 : (cov : (* (OX CX)) covers L ) → ¬ ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) 
+          f20 = ?
       record  NC : Set n where   -- x is not covered 
         field
            x : Ordinal