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

diff -r 2479884b35b2 -r b45925515f77 src/Topology.agda
--- a/src/Topology.agda	Fri Jan 20 17:02:09 2023 +0900
+++ b/src/Topology.agda	Fri Jan 20 22:33:30 2023 +0900
@@ -39,7 +39,7 @@
        OS    : HOD
        OS⊆PL :  OS ⊆ Power L
        o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q      → OS ∋ (p ∩ q)
-       o∪ : { P : HOD }  →  P ⊂ OS                → OS ∋ Union P
+       o∪ : { P : HOD }  →  P ⊆ OS                → OS ∋ Union P
        OS∋od∅ : OS ∋ od∅
 --- we may add
 --     OS∋L   :  OS ∋ L
@@ -57,11 +57,11 @@
         lem0 : L ＼ * (& L) ≡ od∅
         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 
+   CS⊆PL {x} Cx y xy = proj1 Cx xy
    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  
+   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
@@ -75,19 +75,34 @@
         → 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
+record NAO {L : HOD} (top : Topology L) (A : HOD) (A⊆L : A ⊆ L) (o : Ordinal) : Set n where
    field
-       ox : odef (OS top) x
-       na : ¬ ( A ⊆ * x)
+       ox : odef (OS top) o
+       na : ¬ ( A ⊆ * o)
 
 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 = ⟪ ? , ? ⟫
+   NCl⊆OS : NCl ⊆ OS top
+   NCl⊆OS {x} ncl = NAO.ox ncl
    ccl00 : (L ＼ (Cl top A A⊆L)) ≡ Union NCl
-   ccl00 =  ==→o≡ ( record { eq→ = ? ; eq← = ? } )
+   ccl00 =  ==→o≡ ( record { eq→ = ccl01 ; eq← = ? } ) where
+       ccl01 : {x : Ordinal} → odef (L ＼ Cl top A A⊆L) x → odef (Union NCl) x
+       ccl01 {x} ⟪ Lx , nclx ⟫ with ODC.∋-p O A (* x)
+       ... | yes A∋x = ⊥-elim ( nclx ⟪ Lx , (λ c cc ac → ac (subst (λ k → odef A k) &iso  A∋x) ) ⟫  )
+       ... | no ¬A∋x with ODC.p∨¬p O (NCl =h= od∅)
+       ... | case1 ¬nao = ?
+       ... | case2 nao = record { owner = & o ; ao = ODC.x∋minimal O NCl nao ; ox = subst (λ k → odef k x) (sym *iso) ccl02  } where
+            o = minimal NCl nao
+            ccl02 :  odef o x 
+            ccl02 with ODC.∋-p O o (* x)
+            ... | yes y = subst (λ k → odef o k) &iso y
+            ... | no ¬ox  = ⊥-elim ( nclx ⟪ Lx , ? ⟫ )
+               --   not A∋x, ¬ ( A ⊆  o) → A ⊆ (L ＼ o) → (L ＼ o) ∋ x
+               -- ¬ox → (L ＼ o) ∋ x, A ⊆ (L ＼ o) → 
+               -- ⊥-elim ( NAO.na (ODC.x∋minimal O NCl nao) ( λ oa → ⊥-elim ( nclx ⟪ Lx , (λ c cc ac → ? ) ⟫ )))
+
 
 -- Subbase P
 --   A set of countable intersection of P will be a base (x ix an element of the base)
@@ -113,17 +128,17 @@
 
 --  An open set generate from a base
 --
---  OS = { U ⊂ L | ∀ x ∈ U → ∃ b ∈ P →  x ∈ b ⊂ U }
+--  OS = { U ⊆ L | ∀ x ∈ U → ∃ b ∈ P →  x ∈ b ⊆ U }
 
 record Base (L P : HOD) (u x : Ordinal) : Set n where
    field
        b   : Ordinal
-       u⊂L : * u ⊆ L
+       u⊆L : * u ⊆ L
        sb  : Subbase P b
        b⊆u : * b ⊆ * u
        bx  : odef (* b) x
    x⊆L : odef L x
-   x⊆L = u⊂L (b⊆u bx)
+   x⊆L = u⊆L (b⊆u bx)
 
 SO : (L P : HOD) → HOD
 SO L P = record { od = record { def = λ u → {x : Ordinal } → odef (* u) x → Base L P u x } ; odmax = osuc (& L) ; <odmax = tp00 } where
@@ -135,7 +150,7 @@
        P⊆PL   : P ⊆ Power L
 --  we may need these if OS ∋ L is necessary
 --     p    : {x : HOD} → L ∋ x → HOD
---     Pp : {x : HOD} → {lx : L ∋ x } → P ∋ p lx
+--     Pp   : {x : HOD} → {lx : L ∋ x } → P ∋ p lx
 --     px   : {x : HOD} → {lx : L ∋ x } → p lx ∋ x
 
 InducedTopology : (L P : HOD) → IsSubBase L P  → Topology L
@@ -145,9 +160,9 @@
     tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) *iso (sym &iso) 0x ))
     tp00 : SO L P ⊆ Power L
     tp00 {u} ou x ux  with ou ux
-    ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊂L (b⊆u bx)
+    ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊆L (b⊆u bx)
     tp01 :  {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q)
-    tp01 {p} {q} op oq {x} ux =  record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) ul
+    tp01 {p} {q} op oq {x} ux =  record { b = b ; u⊆L = subst (λ k → k ⊆ L) (sym *iso) ul
       ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx))   ; b⊆u = tp08 ; bx = tp14 } where
         px : odef (* (& p)) x
         px = subst (λ k → odef k x ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) )
@@ -168,17 +183,17 @@
         tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x
         tp14 = subst (λ k → odef k x ) (sym *iso) ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫
         ul :  (p ∩ q) ⊆ L
-        ul = subst (λ k → k ⊆ L ) *iso (λ {z} pq →  (Base.u⊂L (op px)) (pz pq) )  where
+        ul = subst (λ k → k ⊆ L ) *iso (λ {z} pq →  (Base.u⊆L (op px)) (pz pq) )  where
             pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z
             pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) )
-    tp02 : { q : HOD} → q ⊂ SO L P → SO L P ∋ Union q
-    tp02 {q} q⊂O {x} ux with subst (λ k → odef k x) *iso ux
-    ... | record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx
-    ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊂L = subst (λ k → k ⊆ L) (sym *iso) tp04
+    tp02 : { q : HOD} → q ⊆ SO L P → SO L P ∋ Union q
+    tp02 {q} q⊆O {x} ux with subst (λ k → odef k x) *iso ux
+    ... | record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx
+    ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊆L = subst (λ k → k ⊆ L) (sym *iso) tp04
            ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) tp06  ; bx = bx } where
         tp05 :  Union q ⊆ L
-        tp05 {z} record { owner = y ; ao = qy ; ox = yx } with proj2 q⊂O qy yx
-        ... | record { b = b ; u⊂L = u⊂L ; sb = sb ; b⊆u = b⊆u ; bx = bx }
+        tp05 {z} record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx
+        ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx }
            = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx ))
         tp04 :  Union q ⊆ L
         tp04 = tp05
@@ -449,29 +464,29 @@
 -- filter Base
 record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
    field
-       b x : Ordinal 
+       b x : Ordinal
        b⊆X : * b ⊆ * X
-       sb  : Subbase (* b) x 
+       sb  : Subbase (* b) x
        u⊆P : * u ⊆ P
        x⊆u : * x ⊆ * u
 
 open import maximum-filter O
 
-UFLP→FIP : {P : HOD} (TP : Topology P) → 
+UFLP→FIP : {P : HOD} (TP : Topology P) →
    ( {L : HOD} (LP : L ⊆ Power P ) → (F : Filter {L} {P} LP ) (UF : ultra-filter F ) → UFLP TP LP F UF ) → FIP TP
 UFLP→FIP {P} TP uflp = record { limit = uf00 ; is-limit = {!!} } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
      fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
      N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
-     N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) 
+     N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
         ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt))  }
      N⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ Power P
      N⊆PP CSX fp nx b xb  = FBase.u⊆P nx xb
      F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {Power P} {P} (λ x → x)
      F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where
          f1 :  {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
-         f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q = 
-                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp → 
+         f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q =
+                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp →
                             subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp)))  } where
               f10 : q ⊆ P
               f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx  ))
@@ -488,7 +503,7 @@
               ... | case1 np = FBase.b⊆X Np np
               ... | case2 nq = FBase.b⊆X Nq nq
               f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
-              f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq 
+              f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
                  → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
      proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ¬ (N CSX fp ∋ od∅)
      proper = ?
@@ -498,7 +513,7 @@
      maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
      maxf {X} CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp)
      uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
-     uf00 {X} CSX fp = UFLP.limit ( uflp (λ x → x) 
+     uf00 {X} CSX fp = UFLP.limit ( uflp (λ x → x)
          ( MaximumFilter.mf (maxf CSX fp) )
          (F→ultra {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp)  ? ? (proper CSX fp)))
 
@@ -539,7 +554,7 @@
              ty00 :  Proj1PP (filter F) (Power P) (Power Q) ⊆ LP
              ty00 {x} ⟪ PPx , ppf ⟫ = ⟪ PPx , ( λ y → record { pq = PProj1.pq (ppf y)
                  ; opq = PProj1.opq (ppf y) ; Lpq = f⊆L F (PProj1.Lpq (ppf y)) ; x=pi1 = PProj1.x=pi1 (ppf y) } )  ⟫
-         UFP : ultra-filter FP 
+         UFP : ultra-filter FP
          UFP = record { proper = ? ; ultra = ? }
          uflp : UFLP TP LPP FP UFP
          uflp = FIP→UFLP TP (Compact→FIP TP CP) LPP FP UFP