# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677145487 -32400
# Node ID 8e04e3cad0b5b98fdfdb022fb9a7fe4a3b5ea5af
# Parent  f4cd937759fce212e3d3fe0ed2abe72c1ecf3ca6
...

diff -r f4cd937759fc -r 8e04e3cad0b5 src/OD.agda
--- a/src/OD.agda	Thu Feb 23 12:48:00 2023 +0800
+++ b/src/OD.agda	Thu Feb 23 18:44:47 2023 +0900
@@ -400,6 +400,10 @@
 power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
 power← A t t⊆A z xz = subst (λ k → odef A k ) &iso ( t⊆A  (subst₂ (λ j k → odef j k) *iso (sym &iso) xz ))
 
+Intersection : (X : HOD ) → HOD   -- ∩ X
+Intersection X = record { od = record { def = λ x → (x o< & X ) ∧ ( {y : Ordinal} → odef X y → odef (* y) x )} ; odmax = & X ; <odmax = λ lt → proj1 lt } 
+
+
 -- ｛_｝ : ZFSet → ZFSet
 -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
 
diff -r f4cd937759fc -r 8e04e3cad0b5 src/Topology.agda
--- a/src/Topology.agda	Thu Feb 23 12:48:00 2023 +0800
+++ b/src/Topology.agda	Thu Feb 23 18:44:47 2023 +0900
@@ -446,8 +446,10 @@
             fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w
             fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
 
+open _==_
+
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
-Compact→FIP {L} top fip with trio< (& L) o∅
+Compact→FIP {L} top compact with trio< (& L) o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? } 
 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
@@ -463,35 +465,31 @@
    --   if all finite intersection of (OX 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
-   --
-   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
-       i01 : HOD
-       i01 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X ) )
-       i02 : odef (* X) (& i01)
-       i02 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X ) )
-       i00 : {x : Ordinal} → ({y : Ordinal} → odef (* X) y → odef (* y) x) → x o< osuc X
-       i00 {x} xy = begin
-           x ≡⟨ sym &iso  ⟩
-           & (* x) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) i03)  ⟩
-           & i01 <⟨ c<→o< i02  ⟩
-           & (* X) ≡⟨ &iso  ⟩
-           X ∎ where 
-               open o≤-Reasoning O
-               i03 : odef (* (& i01)) x
-               i03 = xy i02
    has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
-      →  ¬ (  Intersection X ? =h= od∅ )
-   has-intersection {X} CX fip i=0 = ? where
+      → 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 = ?
        no-cover : ¬ ( (* (OX CX)) covers L ) 
-       no-cover = ?
+       no-cover cov = ⊥-elim ( o<¬≡ ? (fip ? ?)  ) where
+          fp01 : Ordinal
+          fp01 = Compact.finCover compact (OOX CX) cov
+          fp02 : Subbase ? ?
+          fp02 = ?
    limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
       → Ordinal
-   limit = ?
+   limit {X} CX fip with trio< X o∅ 
+   ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
+   ... | tri≈ ¬a b ¬c = o∅
+   ... | tri> ¬a ¬b c = & (ODC.minimal O (Intersection (* X)) ( has-intersection CX fip c))
    fip00 : {X : Ordinal} (CX : * X ⊆ CS top)
             (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
             {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip )
-   fip00 = ?
+   fip00 {X} CX fip {x} Xx with trio< X o∅
+   ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
+   ... | tri≈ ¬a b ¬c = ⊥-elim (  o<¬≡ (sym b) (subst (λ k → o∅ o< k) &iso (∈∅< Xx) ) )
+   ... | tri> ¬a ¬b c with ODC.x∋minimal O (Intersection (* X)) ( has-intersection CX fip c )
+   ... | ⟪ 0<m , intersect ⟫ = intersect Xx 
 
 
 open Filter