# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677028260 -32400
# Node ID ae586d6275c2a5de4d6206fea869874f3b38e914
# Parent  7d2bae0ff36bd8186b368c7c5e1a3e12b7bbd8af
...

diff -r 7d2bae0ff36b -r ae586d6275c2 src/Topology.agda
--- a/src/Topology.agda	Tue Feb 21 12:02:41 2023 +0900
+++ b/src/Topology.agda	Wed Feb 22 10:11:00 2023 +0900
@@ -464,10 +464,14 @@
    --   there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
    --     it means there is a limit
    --
-   Intersection : (X : Ordinal ) →  HOD
-   Intersection X = record { od = record { def = λ x → {y : Ordinal} → odef (* X) y → odef (* y) x } ; odmax = ? ; <odmax = ? }
+   Intersection : (X : Ordinal ) → o∅ o< X →  HOD   -- ∩ X
+   Intersection X 0<X = record { od = record { def = λ x → {y : Ordinal} → odef (* X) y → odef (* y) x } ; odmax = osuc X ; <odmax = i00 } where
+       i00 : {x : Ordinal} → ({y : Ordinal} → odef (* X) y → odef (* y) x) → x o< osuc X
+       i00 {x} xy = begin
+           x ≤⟨ ? ⟩
+           X ∎ where open o≤-Reasoning O
    has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
-      →  ¬ (  Intersection X  =h= od∅ )
+      →  ¬ (  Intersection X ? =h= od∅ )
    has-intersection {X} CX fip i=0 = ? where
        no-cover : ¬ ( (* (OX CX)) covers L ) 
        no-cover = ?