# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677034869 -32400
# Node ID 66355bace86f4908770c3254ab70f2f3f5d1c88f
# Parent  ae586d6275c2a5de4d6206fea869874f3b38e914
...

diff -r ae586d6275c2 -r 66355bace86f src/Topology.agda
--- a/src/Topology.agda	Wed Feb 22 10:11:00 2023 +0900
+++ b/src/Topology.agda	Wed Feb 22 12:01:09 2023 +0900
@@ -277,6 +277,15 @@
           →  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 fip (λ x → x) (gi ?)
+... | t = ?
+
+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 = ?
+
 -- Compact
 
 data Finite-∪ (S : HOD) : Ordinal → Set n where