# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677335974 -32400
# Node ID ffe5bc98f9d1ea254e8c0082431bdfb38d880f34
# Parent  807a55d550866acddd84014f0388ace066be7776
not-covered

diff -r 807a55d55086 -r ffe5bc98f9d1 src/OD.agda
--- a/src/OD.agda	Sat Feb 25 19:30:43 2023 +0900
+++ b/src/OD.agda	Sat Feb 25 23:39:34 2023 +0900
@@ -401,7 +401,7 @@
 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 } 
+Intersection X = record { od = record { def = λ x → (x o≤ & X ) ∧ ( {y : Ordinal} → odef X y → odef (* y) x )} ; odmax = osuc (& X) ; <odmax = λ lt → proj1 lt } 
 
 
 -- ｛_｝ : ZFSet → ZFSet
diff -r 807a55d55086 -r ffe5bc98f9d1 src/Topology.agda
--- a/src/Topology.agda	Sat Feb 25 19:30:43 2023 +0900
+++ b/src/Topology.agda	Sat Feb 25 23:39:34 2023 +0900
@@ -467,26 +467,32 @@
    --     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 =  ⊥-elim ( ¬x<0 {NC.x fp13} ( eq→ i=0 ⟪ fp06 , fp05  ⟫ )) where
+   has-intersection {X} CX fip 0<X i=0 =  ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05  ⟫ )) where
+      fp07 : HOD  -- we have an element of X
+      fp07 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
+      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 ( o<¬≡ ? (fip ? ?)  ) where
+      no-cover cov = ⊥-elim ( o<¬≡ ? (fip (λ x → x) (fp02 (Compact.isFinite compact (OOX CX) cov)))  ) where
           fp01 : Ordinal
           fp01 = Compact.finCover compact (OOX CX) cov
-          fp02 : Subbase ? ?
+          int : HOD
+          int = Replace (* fp01) (λ x → L ＼ x)
+          fp02 : Finite-∪ (* (OX CX)) fp01 → Subbase (* X) (& (Intersection (Replace (* fp01) (λ x → L ＼ x))))
           fp02 = ?
-      record  NC : Set n where
+          fp03 : * (& (Replace (* fp01) (λ x → L ＼ x))) ⊆ * X
+          fp03 = ?
+      record  NC : Set n where   -- x is not covered 
         field
            x : Ordinal
-           Lx : odef L x
            yx : {y : Ordinal} (Xy : odef (* X) y) →  odef (* y) x 
-      fp13 : NC 
-      fp13 with ODC.p∨¬p O NC 
+      not-covered : NC 
+      not-covered with ODC.p∨¬p O NC 
       ... | case1 nc = nc 
       ... | case2 ¬nc = ⊥-elim ( no-cover record { cover = λ Lx → & (L ＼ coverf Lx) ; P∋cover = fp22 ; isCover = fp23 } ) where
-          fp14 : {x : Ordinal} → odef L x → ¬ ( {y : Ordinal} → odef (* X) y →  odef (* y) x  )
-          fp14 {x} Lx yx = ¬nc record { x =  x ; Lx = Lx ;  yx = yx  }
           coverSet : {x : Ordinal} → odef L x → HOD
-          coverSet {x} Lx = record { od = record { def = λ y → odef (* X) y ∧ odef (L ＼ * y) x } ; odmax = ? ; <odmax = ? }
+          coverSet {x} Lx = record { od = record { def = λ y → odef (* X) y ∧ odef (L ＼ * y) x } ; odmax = X 
+             ; <odmax = λ {x} lt → subst (λ k → x o< k) &iso ( odef< (proj1 lt)) }
           fp17 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( coverSet Lx =h= od∅ )
           fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; Lx = Lx ; yx = fp19 } ) where
              fp19 : {y : Ordinal} → odef (* X) y → odef (* y) x
@@ -497,20 +503,24 @@
                 fp20 = ⟪ Xy , lyx ⟫
           coverf : {x : Ordinal} → (Lx : odef L x ) → HOD
           coverf Lx =  ODC.minimal O (coverSet Lx) (fp17 Lx)
-          fp22 : {x : Ordinal} (lt : odef L x) → odef (* (OX CX)) (& (coverf lt))
-          fp22 {x} Lx = subst ( λ k → odef k (& (coverf Lx))) (sym *iso) ( record { z = & (coverf Lx) ; az = fp25 ; x=ψz = ? } ) where
-             fp24 : & (coverf Lx) ≡ & (L ＼ *  ? )
-             fp24 = ?
+          fp22 :  {x : Ordinal} (lt : odef L x) → odef (* (OX CX)) (& (L ＼ coverf lt))
+          fp22 {x} Lx = subst (λ k → odef k (& (L ＼ coverf Lx ))) (sym *iso) record { z = _ ; az = fp25 ; x=ψz = fp24   } where
+             fp24 : & (L ＼ coverf Lx) ≡ & (L ＼ * (& (coverf Lx)))
+             fp24 = cong (λ k → & ( L ＼ k )) (sym *iso)
              fp25 : odef (* X) (& (coverf Lx))
              fp25 = proj1 ( ODC.x∋minimal O (coverSet Lx) (fp17 Lx) )
-          -- with ( ODC.x∋minimal O (coverSet Lx) (fp17 Lx) )
-          -- ... | t = ?
-          fp23 : {x : Ordinal} (lt : odef L x) → odef (* (& (coverf lt))) x
-          fp23 {x} Lx = ?
-      fp05 : {y : Ordinal } → (Xy : odef (* X) y ) → odef ( * y) (NC.x fp13 )
-      fp05 {y} Xy = NC.yx fp13 Xy
-      fp06 : NC.x fp13 o< & (* X)
-      fp06 = ?
+          fp23 :  {x : Ordinal} (lt : odef L x) → odef (* (& (L ＼ coverf lt))) x
+          fp23 {x} Lx = subst (λ k → odef k x) (sym *iso) ⟪ Lx , fp26 ⟫  where
+             fp26 : ¬ odef (coverf Lx) x
+             fp26 = subst (λ k → ¬ odef k x ) *iso (proj2 (proj2 ( ODC.x∋minimal O (coverSet Lx) (fp17 Lx) ))  )
+      fp05 : {y : Ordinal } → (Xy : odef (* X) y ) → odef ( * y) (NC.x not-covered )
+      fp05 {y} Xy = NC.yx not-covered Xy
+      fp06 : NC.x not-covered o≤ & (* X)
+      fp06 = begin
+         NC.x not-covered ≡⟨ sym &iso ⟩
+         & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered fp08)) ⟩
+         & fp07  <⟨ c<→o< fp08 ⟩
+         & (* X) ∎ where open o≤-Reasoning O
    limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
       → Ordinal
    limit {X} CX fip with trio< X o∅