# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673791356 -32400
# Node ID 73b256c5474b5c585678b4c59a51e7f3c7ac0e8e
# Parent  2fe1bc2b962f02464677c24911cdef15f82b1d13
...

diff -r 2fe1bc2b962f -r 73b256c5474b src/Topology.agda
--- a/src/Topology.agda	Sun Jan 15 19:30:21 2023 +0900
+++ b/src/Topology.agda	Sun Jan 15 23:02:36 2023 +0900
@@ -273,28 +273,45 @@
       field
          is-CS : * x ⊆ CS top
          y : Ordinal 
-         ¬fip  : {y : Ordinal } →  Subbase (* x) y →  o∅ ≡ y 
+         sy :  Subbase (* y)  o∅ 
    Cex : HOD
    Cex = record { od = record { def = λ x → CFIP x } ; odmax = osuc (& (CS top)) ; <odmax = λ {x} lt → 
         subst₂ (λ j k → j o≤ k ) &iso refl ( ⊆→o≤ (CFIP.is-CS lt )) }
    cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
    cex {X} ox oc = & ( ODC.minimal O Cex  fip00)  where
       fip00 : ¬ ( Cex  =h= od∅ ) 
-      fip00 cex=0 = fip03 (FIP.is-limit fip (CCX ox) fip02 ?) {!!} where 
+      fip00 cex=0 = fip03 (FIP.is-limit fip (CCX ox) fip02 fip07 ) fip09 where 
           fip03 : {x z : Ordinal } → odef (* x) z →  (¬ odef (* x) z) → ⊥
           fip03 {x} {z} xz nxz = nxz xz
           fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
           fip02 {C} {x} C<CX sc with trio< x o∅ 
           ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
           ... | tri> ¬a ¬b c = c
-          ... | tri≈ ¬a b ¬c  = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; y = x ; ¬fip = ? } )) where
+          ... | tri≈ ¬a b ¬c  = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; y = C ; sy = subst (λ k → Subbase (* C) k) b sc } )) where
               fip10 : * C ⊆  CS top
-              fip10 {w} cw with subst (λ k → odef k w) *iso ( C<CX cw )
-              ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ ? , ? ⟫
+              fip10 {w} cw = CCX ox ( C<CX cw )
           fip01 : Ordinal
           fip01 = FIP.limit fip (CCX ox) fip02
+          fip11 :  {w : Ordinal } → {Lw : odef L  w} → ¬ ( odef (* (cover oc Lw)) w )
+          fip11 {w} {Lw} pw = ? where
+                fip15 : odef (* X) (cover oc Lw)
+                fip15 = P∋cover oc {w} {Lw}
+                fip13 : HOD
+                fip13 = L ＼ * w
+                fip14 : odef (* (CX ox)) (& ( L ＼ * w ))
+                fip14 = ?
+                fip12 : odef ( L ＼ * w ) fip01
+                fip12 = subst (λ k → odef k fip01 ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip14 )
+          fip10 : odef ? fip01
+          fip10 = FIP.is-limit fip (CCX ox) fip02 ?
+          fip08 : odef L fip01
+          fip08 = FIP.L∋limit fip (CCX ox) fip02 ?
           fip05 : odef (CS top) fip01 
           fip05 = ?
+          fip07 : odef (* (CX ox)) ( cover oc fip08  )
+          fip07 = ?
+          fip09 : ¬ odef (* (cover oc fip08)) (FIP.limit fip (CCX ox) fip02)
+          fip09 = ?
           fip04 : Ordinal
           fip04 = cover oc (cs⊆L top (subst₂ (λ j k → odef j k ) refl (sym &iso) fip05) (FIP.is-limit fip (CCX ox) ? ?) )
    ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅