# HG changeset patch
# User kono
# Date 1677210764 -28800
# Node ID cf25490dd112877c736fa0afff8ae3c22edb4ba6
# Parent  8e04e3cad0b5b98fdfdb022fb9a7fe4a3b5ea5af
...

diff -r 8e04e3cad0b5 -r cf25490dd112 src/Topology.agda
--- a/src/Topology.agda	Thu Feb 23 18:44:47 2023 +0900
+++ b/src/Topology.agda	Fri Feb 24 11:52:44 2023 +0800
@@ -467,9 +467,15 @@
    --     it means there is a limit
    has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
       → o∅ o< X  →  ¬ (  Intersection (* X) =h= od∅ )
-   has-intersection {X} CX fip 0<X i=0 = no-cover record { cover = cover1 ; P∋cover = ? ; isCover = ? } where
-       cover1 :  {x : Ordinal} → odef L x → Ordinal
-       cover1 {x} Lx = ?
+   has-intersection {X} CX fip 0<X i=0 = no-cover record { cover = ? ; P∋cover = ? ; isCover = ? } where
+       cover1 :  {x : Ordinal} → odef L x → Own (* (OX CX)) x
+       cover1 {x} Lx with ODC.p∨¬p O (Own (* (OX CX)) x)
+       ... | case1 p = p
+       ... | case2 np = ⊥-elim ( ¬x<0 ( eq→ i=0 ⟪ ? , ? ⟫ )) where
+          fp04 : {y : Ordinal} → odef (* X) y → Ordinal
+          fp04 {y} xy = & (L ＼ * y)
+          fp03 : ?
+          fp03 = ?
        no-cover : ¬ ( (* (OX CX)) covers L ) 
        no-cover cov = ⊥-elim ( o<¬≡ ? (fip ? ?)  ) where
           fp01 : Ordinal