# HG changeset patch
# User kono
# Date 1677127680 -28800
# Node ID f4cd937759fce212e3d3fe0ed2abe72c1ecf3ca6
# Parent  7bd348551d37292bdca86b62bfaec50375c39ba1
...

diff -r 7bd348551d37 -r f4cd937759fc src/Topology.agda
--- a/src/Topology.agda	Thu Feb 23 09:58:11 2023 +0800
+++ b/src/Topology.agda	Thu Feb 23 12:48:00 2023 +0800
@@ -277,22 +277,6 @@
           →  odef L (limit CX fip)
    L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx)
 
-fipx : {L : HOD} (top : Topology L) → {X : Ordinal } → * X ⊆ CS top
-     →   ( { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  Ordinal
-fipx {L} top {X} X⊆CS fip with trio< X o∅ 
-... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-... | tri≈ ¬a b ¬c = o∅
-... | tri> ¬a ¬b c = & (ODC.minimal O (* fip00) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) ( fip (λ x → x ) (gi ? ) )))) where
-   fip00 : ?
-   fip00 = & (ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) c ) )) 
-
-fipX∋x : {L : HOD} (top : Topology L) → {X : Ordinal } → (X⊆CS : * X ⊆ CS top )
-     →   (fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  odef (* X) (fipx top X⊆CS fip)
-fipX∋x {L} top {X} X⊆CS fip with trio< X o∅ 
-... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-... | tri≈ ¬a b ¬c = ?
-... | tri> ¬a ¬b c = ? -- fip (λ x → x) (gi ?)
-
 -- Compact
 
 data Finite-∪ (S : HOD) : Ordinal → Set n where
@@ -482,10 +466,20 @@
    --
    Intersection : (X : Ordinal ) → o∅ o< X →  HOD   -- ∩ X
    Intersection X 0<X = record { od = record { def = λ x → {y : Ordinal} → odef (* X) y → odef (* y) x } ; odmax = osuc X ; <odmax = i00 } where
+       i01 : HOD
+       i01 = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X ) )
+       i02 : odef (* X) (& i01)
+       i02 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X ) )
        i00 : {x : Ordinal} → ({y : Ordinal} → odef (* X) y → odef (* y) x) → x o< osuc X
        i00 {x} xy = begin
-           x ≤⟨ ? ⟩
-           X ∎ where open o≤-Reasoning O
+           x ≡⟨ sym &iso  ⟩
+           & (* x) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) i03)  ⟩
+           & i01 <⟨ c<→o< i02  ⟩
+           & (* X) ≡⟨ &iso  ⟩
+           X ∎ where 
+               open o≤-Reasoning O
+               i03 : odef (* (& i01)) x
+               i03 = xy i02
    has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
       →  ¬ (  Intersection X ? =h= od∅ )
    has-intersection {X} CX fip i=0 = ? where