# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674201729 -32400
# Node ID 2479884b35b267aa4f59c6bc8fe20d466eae5acf
# Parent  adba530ce1f03298d08ba6ef45bd373b04edfcfe
...

diff -r adba530ce1f0 -r 2479884b35b2 src/Topology.agda
--- a/src/Topology.agda	Fri Jan 20 14:40:54 2023 +0900
+++ b/src/Topology.agda	Fri Jan 20 17:02:09 2023 +0900
@@ -41,6 +41,8 @@
        o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q      → OS ∋ (p ∩ q)
        o∪ : { P : HOD }  →  P ⊂ OS                → OS ∋ Union P
        OS∋od∅ : OS ∋ od∅
+--- we may add
+--     OS∋L   :  OS ∋ L
 -- closed Set
    CS : HOD
    CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L ＼ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where
@@ -56,8 +58,11 @@
         lem0 = subst (λ k → L ＼ k  ≡ od∅) (sym *iso) L＼L=0
    CS⊆PL :  CS ⊆ Power L
    CS⊆PL {x} Cx y xy = proj1 Cx xy 
---- we may add
---     OS∋L   :  OS ∋ L
+   P＼CS=OS : {cs : HOD} → CS ∋ cs →  OS ∋ ( L ＼ cs )
+   P＼CS=OS {cs} ⟪ cs⊆L , olcs  ⟫ = subst (λ k → odef OS k) (cong (λ k → & ( L ＼ k)) *iso)  olcs
+   P＼OS=CS : {cs : HOD} → OS ∋ cs →  CS ∋ ( L ＼ cs )
+   P＼OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) (sym *iso) proj1  
+      , subst (λ k → odef OS k) (cong (&) (trans (sym (L＼Lx=x (os⊆L oos))) (cong (λ k → L ＼ k) (sym *iso)) )) oos  ⟫
 
 open Topology
 
@@ -70,6 +75,20 @@
         → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x)))
     ; eq← =  λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } )
 
+record NAO {L : HOD} (top : Topology L) (A : HOD) (A⊆L : A ⊆ L) (x : Ordinal) : Set n where
+   field
+       ox : odef (OS top) x
+       na : ¬ ( A ⊆ * x)
+
+CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → (A⊆L : A ⊆ L) → CS top ∋ Cl top A A⊆L
+CS∋Cl {L} top A A⊆L = ⟪ (λ {x} cx → proj1 ( subst (λ k → odef k x) *iso cx )) , ? ⟫ where
+   NCl : HOD
+   NCl = record { od = record { def = λ x → NAO top A A⊆L x } ; odmax = & (OS top) ; <odmax = λ lt → odef< (NAO.ox lt) }
+   NCl⊂OS : NCl ⊂ OS top 
+   NCl⊂OS = ⟪ ? , ? ⟫
+   ccl00 : (L ＼ (Cl top A A⊆L)) ≡ Union NCl
+   ccl00 =  ==→o≡ ( record { eq→ = ? ; eq← = ? } )
+
 -- Subbase P
 --   A set of countable intersection of P will be a base (x ix an element of the base)
 
@@ -486,6 +505,14 @@
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (UF : ultra-filter F ) → UFLP {P} TP {L} LP F UF
 FIP→UFLP {P} TP fip {L} LP F UF = record { limit = FIP.limit fip ? ? ; P∋limit = ? ; is-limit = ? } where
+     CF : HOD
+     CF = Replace' (filter F) (λ x fx → Cl TP x (λ {w} xw → LP (f⊆L F fx) _ (subst (λ k → odef k w) (sym *iso) xw )) )
+     CF⊆CS : CF ⊆ CS TP
+     CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ subst (λ k → k ⊆ P) (trans (sym *iso) (sym (cong (*) x=ψz))) uf01 , uf02 ⟫ where
+        uf01 : (Cl TP (* z) (λ {w} xw → LP (f⊆L F (subst (odef (filter F)) (sym &iso) az)) w (subst (λ k → odef k w) (sym *iso) xw))) ⊆ P
+        uf01 = ?
+        uf02 : odef (OS TP) (& (P ＼ * x))
+        uf02 = ?
      ufl00 :  {v : Ordinal} → Neighbor TP (FIP.limit fip ? ?) v → filter F ⊆ * v
      ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } = ?