# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677321043 -32400
# Node ID 807a55d550866acddd84014f0388ace066be7776
# Parent  0b2d03711aff34085c156945331da2cb38f5696f
...

diff -r 0b2d03711aff -r 807a55d55086 src/Topology.agda
--- a/src/Topology.agda	Sat Feb 25 15:32:50 2023 +0800
+++ b/src/Topology.agda	Sat Feb 25 19:30:43 2023 +0900
@@ -467,7 +467,7 @@
    --     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 ( eq→ i=0 ⟪ ? , fp05 ⟫ )) where
+   has-intersection {X} CX fip 0<X i=0 =  ⊥-elim ( ¬x<0 {NC.x fp13} ( eq→ i=0 ⟪ fp06 , fp05  ⟫ )) where
       no-cover : ¬ ( (* (OX CX)) covers L ) 
       no-cover cov = ⊥-elim ( o<¬≡ ? (fip ? ?)  ) where
           fp01 : Ordinal
@@ -476,24 +476,41 @@
           fp02 = ?
       record  NC : Set n where
         field
-           x y : Ordinal
+           x : Ordinal
            Lx : odef L x
-           Xy : odef (* X) y 
-           yx : odef (* y) x 
-      fp03 : NC 
-      fp03 with ODC.p∨¬p O NC 
+           yx : {y : Ordinal} (Xy : odef (* X) y) →  odef (* y) x 
+      fp13 : NC 
+      fp13 with ODC.p∨¬p O NC 
       ... | case1 nc = nc 
-      ... | case2 ¬nc = ⊥-elim ( no-cover record { cover = λ Lx → ? ; P∋cover = ? ; isCover = ? } ) where
-          fp14 : {x : Ordinal} → odef L x → {y : Ordinal} → odef (* X) y → ¬ odef (* y) x 
-          fp14 {x} Lx {y} Xy yx = ¬nc record { x =  x ; Lx = Lx ; y = y ; Xy = Xy ; yx = yx }
-          fp06 : {x : Ordinal} → odef L x → HOD
-          fp06 {x} Lx = record { od = record { def = λ y → odef (* X) y → odef (L ＼ * y) x } ; odmax = ? ; <odmax = ? }
-          fp07 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( fp06 Lx =h= od∅ )
-          fp07 {x} Lx eq = ⊥-elim (¬x<0 {x} (eq→ eq fp08)) where
-             fp08 : {y : Ordinal} → odef (* X) y → odef (L ＼ * y) x
-             fp08 = ? 
-      fp05 : {y : Ordinal } → odef (* X) y → odef ( * y) (NC.x fp03)
-      fp05 {y} Xy = ?
+      ... | 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 = ? }
+          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
+             fp19 {y} Xy with ∨L＼X {L} {* y} {x} Lx
+             ... | case1 yx = yx
+             ... | case2 lyx = ⊥-elim ( ¬x<0 {y} ( eq→ eq fp20 )) where
+                fp20 : odef (* X) y ∧ odef (L ＼ * y) x
+                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 = ?
+             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 = ?
    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∅