# HG changeset patch
# User kono
# Date 1677310370 -28800
# Node ID 0b2d03711aff34085c156945331da2cb38f5696f
# Parent  f5deac708524cbb4aed1516526c12f7dd0a6dff6
....

diff -r f5deac708524 -r 0b2d03711aff src/Topology.agda
--- a/src/Topology.agda	Sat Feb 25 11:24:45 2023 +0800
+++ b/src/Topology.agda	Sat Feb 25 15:32:50 2023 +0800
@@ -476,14 +476,24 @@
           fp02 = ?
       record  NC : Set n where
         field
-           nc : Ordinal
-           is-nc : {y : Ordinal} → odef (* (OX CX)) y → ¬ (odef (* y) nc )
-      fp03 : NC
-      fp03 with ODC.p∨¬p O NC
-      ... | case1 nc = nc
-      ... | case2 ¬nc = ⊥-elim ( no-cover record { cover = λ Lx → ? ; P∋cover = ? ; isCover = ? } )
-      fp05 : {y : Ordinal } → odef (* X) y → odef ( * y) ?
-      fp05 = ?
+           x y : Ordinal
+           Lx : odef L x
+           Xy : odef (* X) y 
+           yx : odef (* y) x 
+      fp03 : NC 
+      fp03 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 = ?
    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∅