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

diff -r e110b56d8cbe -r 6174001ba1c0 src/Topology.agda
--- a/src/Topology.agda	Mon Feb 27 07:29:11 2023 +0800
+++ b/src/Topology.agda	Tue Feb 28 15:01:17 2023 +0900
@@ -389,7 +389,13 @@
         fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x)
         fip70 x (gi rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } 
         fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers
-              (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} ? ? ) where
+              (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where
+            fip71 : {a b c : HOD} → a covers c →  (a ∪ b) covers c
+            fip71 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case1 (P∋cover cov lt) 
+               ; isCover = isCover cov } 
+            fip72 : {a b c : HOD} → a covers c →  (b ∪ a) covers c
+            fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt) 
+               ; isCover = isCover cov } 
             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 ⟫ )  ⟫
@@ -424,7 +430,6 @@
    ... | record { z = z ; az = az ; x=ψz = x=ψz } =  subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01))  where
        comp01 : odef (* X) (& (* z))
        comp01 = subst (λ k → odef (* X) k) (sym &iso) az
-
    --   if all finite intersection of X contains something, 
    --   there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
    --     it means there is a limit
@@ -436,17 +441,40 @@
       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 ( ? ) where
+      no-cover cov = ⊥-elim ( SB.¬i⊆Ut (fp02 fp01 (Compact.isFinite compact (OOX CX) cov) ) fp12 ) where
           fp01 : Ordinal
           fp01 = Compact.finCover compact (OOX CX) cov
-          fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L ＼ * t ) )
-          fp02 t fin-e = gi ?
-          fp02 t (fin-i tx ) = gi fp03 where
-              fp03 :  odef (* X) (& (L ＼ * t))
-              fp03 = ?
-          fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (fp02 tx x)  (fp02 ty y ) ) where
-              fp04 :  & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
-              fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where
+          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  
+              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 = ?
+              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
+                   fip34 : * z1 ⊆ L
+                   fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1
+                   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 ＼ * 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
+              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
                   fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt
                   ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫  where
@@ -457,7 +485,21 @@
                   fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt
                   ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso) 
                          ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty))  ⟫ ⟫ 
-
+              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
+              fcov = Compact.isCover compact (OOX CX) cov
+              fp13 : Ordinal 
+              fp13 = SB.i (fp02 fp01 (Compact.isFinite compact (OOX CX) cov))
+              fp16 : {y : Ordinal} → odef (L ＼ * fp13) y → odef L y
+              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))
       record  NC : Set n where   -- x is not covered 
         field
            x : Ordinal