# HG changeset patch
# User kono
# Date 1677222023 -28800
# Node ID 0727cf865ebda0d5cef9de69be59a3187b7eafdf
# Parent  cf25490dd112877c736fa0afff8ae3c22edb4ba6
...

diff -r cf25490dd112 -r 0727cf865ebd src/BAlgebra.agda
--- a/src/BAlgebra.agda	Fri Feb 24 11:52:44 2023 +0800
+++ b/src/BAlgebra.agda	Fri Feb 24 15:00:23 2023 +0800
@@ -58,6 +58,11 @@
     lem06 : {x : Ordinal} → odef L x → odef (L ＼ od∅) x
     lem06 {x} Lx = ⟪ Lx , (λ lt → ¬x<0 lt)  ⟫
 
+∨L＼X : { L X : HOD } → {x : Ordinal } → odef L x → odef X x ∨ odef (L ＼ X) x
+∨L＼X {L} {X} {x} Lx with ODC.∋-p O X (* x)
+... | yes y = case1 ( subst (λ k → odef X k ) &iso y  )
+... | no  n = case2 ⟪ Lx , subst (λ k → ¬ odef X k) &iso n ⟫
+
 
 [a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
diff -r cf25490dd112 -r 0727cf865ebd src/Topology.agda
--- a/src/Topology.agda	Fri Feb 24 11:52:44 2023 +0800
+++ b/src/Topology.agda	Fri Feb 24 15:00:23 2023 +0800
@@ -472,8 +472,8 @@
        cover1 {x} Lx with ODC.p∨¬p O (Own (* (OX CX)) x)
        ... | case1 p = p
        ... | case2 np = ⊥-elim ( ¬x<0 ( eq→ i=0 ⟪ ? , ? ⟫ )) where
-          fp04 : {y : Ordinal} → odef (* X) y → Ordinal
-          fp04 {y} xy = & (L ＼ * y)
+          fp04 : {y x : Ordinal} → odef (* X) y → ¬ odef (L ＼ * y) x
+          fp04 {y} {x} xy ⟪ Lx , nx ⟫ = ?
           fp03 : ?
           fp03 = ?
        no-cover : ¬ ( (* (OX CX)) covers L )