--- a/src/Topology.agda	Wed Jan 04 11:21:55 2023 +0900
+++ b/src/Topology.agda	Mon Jan 09 13:09:30 2023 +0900
@@ -13,8 +13,8 @@
 open import Data.Empty
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
-import BAlgbra
-open BAlgbra O
+import BAlgebra
+open BAlgebra O
 open inOrdinal O
 open OD O
 open OD.OD
@@ -60,7 +60,7 @@
 
 Cl : {L : HOD} → (top : Topology L) → (A : HOD) → A ⊆ L → HOD
 Cl {L} top A A⊆L = record { od = record { def = λ x → (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x  } 
-  ; odmax = & L ; <odmax = ? }
+  ; odmax = & L ; <odmax = {!!} }
 
 ClL : {L : HOD} → (top : Topology L) → {f : L ⊆ L } → Cl top L f ≡ L
 ClL {L} top {f} =  ==→o≡ ( record { eq→ = λ {x} ic 
@@ -203,37 +203,37 @@
    CX : {X : Ordinal} → * X ⊆ OS top → Ordinal
    CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
    CCX : {X : Ordinal} → (os :  * X ⊆ OS top) → * (CX os) ⊆ CS top 
-   CCX {X} ox = ?
+   CCX {X} ox = {!!}
    -- CX has finite intersection
    CXfip : {X : Ordinal } → * X ⊆ OS top → Set n
    CXfip {X} ox =  { x C : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x 
    Cex : {X : Ordinal } → * X ⊆ OS top → HOD
    Cex {X} ox =  record { od = record { def = λ C → { x : Ordinal } → * C ⊆ * (CX ox) → Subbase (* C) o∅ } 
-       ; odmax = osuc ( & (Power L)) ; <odmax = ? }
+       ; odmax = osuc ( & (Power L)) ; <odmax = {!!} }
    -- a counter example of fip , some CX has no finite intersection
    cex : {X : Ordinal } → * X ⊆ OS top → * X covers L → Ordinal
    cex {X} ox oc = & ( ODC.minimal O (Cex ox) fip00)  where
       fip00 : ¬ ( Cex ox =h= od∅ ) 
-      fip00 cex=0 = fip03 ? ? where 
+      fip00 cex=0 = fip03 {!!} {!!} where 
           fip03 : {x z : Ordinal } → odef (* x) z →  (¬ odef (* x) z) → ⊥
           fip03 {x} {z} xz nxz = nxz xz
           fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
-          fip02 = ?
+          fip02 = {!!}
           fip01 : Ordinal
-          fip01 = FIP.limit fip (CCX ox) ? fip02
+          fip01 = FIP.limit fip (CCX ox) {!!} fip02
    ¬CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → * (cex ox oc) ⊆ * (CX ox) → Subbase (* (cex ox oc)) o∅ 
-   ¬CXfip {X} ox oc = ? where
+   ¬CXfip {X} ox oc = {!!} where
       fip04 : odef (Cex ox) (cex ox oc)
-      fip04 = ?
+      fip04 = {!!}
    -- this defines finite cover
    finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
    finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L ＼  z ))
    -- create Finite-∪ from cex
    isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
-   isFinite = ?
+   isFinite = {!!}
    -- is also a cover
    isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
-   isCover1 = ?
+   isCover1 = {!!}
 
 
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
@@ -287,7 +287,7 @@
 -- Ultra Filter has limit point
 
 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  
-      (FL : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) : Set (suc (suc n)) where
+      (FL : filter F ∋ P) : Set (suc (suc n)) where
    field
        limit : Ordinal
        P∋limit : odef P limit
@@ -296,9 +296,11 @@
 -- FIP is UFL
 
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
-   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F FP uf
-FIP→UFLP {P} TP fip {L} LP F FP uf = record { limit = FIP.limit fip fip00 CFP fip01  ; P∋limit = FIP.L∋limit fip fip00 CFP fip01 ; is-limit = fip02 }
+   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P)  → UFLP TP LP F FP 
+FIP→UFLP {P} TP fip {L} LP F FP = record { limit = FIP.limit fip fip00 CFP fip01  ; P∋limit = FIP.L∋limit fip fip00 CFP fip01 ; is-limit = fip02 }
     where
+      uf : ultra-filter {L} {P} {LP} F
+      uf = {!!}
       fip03 : {z : HOD} → filter F ∋ z → z ⊆ P
       fip03 {z} fz {x} zx = LP ( f⊆L F fz ) x (subst (λ k → odef k x) (sym *iso) zx  )
       CF : Ordinal
@@ -306,29 +308,36 @@
       CFP : * CF ∋ P  -- filter F ∋ P and Cl P ≡ P
       CFP = subst₂ (λ j k → odef j k) (sym *iso) refl record { z = & P ; az = FP ; x=ψz =  cong (&) fip04 }  where
            fip04 : P ≡ (Cl TP (* (& P)) (fip03 (subst (odef (filter F)) (sym &iso) FP)))
-           fip04 =  ==→o≡ ( record { eq→ = ? ;  eq← =  ?  } )
+           fip04 =  ==→o≡ ( record { eq→ = {!!} ;  eq← =  {!!}  } )
       fip00 : * CF ⊆ CS TP -- replaced
-      fip00 = ?
+      fip00 = {!!}
       fip01 : {C x : Ordinal} → * C ⊆ * CF → Subbase (* C) x → o∅ o< x
-      fip01 {C} {x} CCF (gi Cx) = ? -- filter is proper .i.e it contains no od∅
-      fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = ?
+      fip01 {C} {x} CCF (gi Cx) = {!!} -- filter is proper .i.e it contains no od∅
+      fip01 {C} {.(& (* _ ∩ * _))} CCF (g∩ sb sb₁) = {!!}
       fip02 : {o : Ordinal} → odef (OS TP) o → odef (* o) (FIP.limit fip fip00 CFP fip01) → * o ⊆ filter F
-      fip02 {p} oo ol = ? where
-         fip04 : odef ? (FIP.limit fip fip00 CFP fip01) 
-         fip04 = FIP.is-limit fip fip00 CFP fip01 ?
+      fip02 {p} oo ol {x} ox = fip06 where
+         fip04 : odef {!!} (FIP.limit fip fip00 CFP fip01) 
+         fip04 = FIP.is-limit fip fip00 CFP fip01 {!!}
+         fip05 : ( filter F ∋ (* x) ) ∨ (  filter F ∋ ( P ＼ (* x))  )
+         fip05  = ultra-filter.ultra uf {!!} {!!} 
+         fip06 : odef (filter F) x
+         fip06 with fip05
+         ... | case1 lt = subst (λ k → odef (filter F) k ) &iso lt
+         ... | case2 nlt = {!!}
 
 
 UFLP→FIP : {P : HOD} (TP : Topology P) →
-   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F FP uf ) → FIP TP
-UFLP→FIP {P} TP uflp = record { limit = ? ; is-limit = ? }
+   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP ) (FP : filter F ∋ P) → UFLP TP LP F FP ) → FIP TP
+UFLP→FIP {P} TP uflp = record { limit = {!!} ; is-limit = {!!} }
 
--- Product of UFL has limit point (Tychonoff)
+-- product topology of compact topology is compact
 
 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (TP Top⊗ TQ)
 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where
+    -- Product of UFL has limit point 
     uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ) (LF : filter F ∋ ZFP P Q)
-            (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F ? uf
-    uflp {L} LPQ F LF uf = record { limit = & < * ( UFLP.limit uflpp) , ? >  ; P∋limit = ? ; is-limit = ? } where
+             → UFLP (TP Top⊗ TQ) LPQ F {!!} 
+    uflp {L} LPQ F LF = record { limit = & < * ( UFLP.limit uflpp) , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} } where
          LP : (L : HOD ) (LPQ : L ⊆ Power (ZFP P Q)) → HOD
          LP L LPQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
          LPP : (L : HOD) (LPQ : L ⊆ Power (ZFP P Q)) → LP L LPQ ⊆ Power P
@@ -340,15 +349,13 @@
                     tp03 : odef (* z) z1 →  odef (* (& (* z))) (& (* z1))
                     tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt)
          FP : Filter (LPP L LPQ)
-         FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = ? ; filter2 = ? } where
+         FP = record { filter = LP (filter F) (λ x → LPQ (f⊆L F x )) ; f⊆L = tp04 ; filter1 = {!!} ; filter2 = {!!} } where
              tp04 : LP (filter F) (λ x → LPQ (f⊆L F x )) ⊆ LP L LPQ
-             tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = ? }
-         uFP : ultra-filter FP
-         uFP = record { proper = ? ; ultra = ? }
-         uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP ? uFP
-         uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP ? uFP
+             tp04 record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = f⊆L F az ; x=ψz = {!!} }
+         uflpp : UFLP {P} TP {LP L LPQ} (LPP L LPQ) FP {!!} 
+         uflpp = FIP→UFLP TP (Compact→FIP TP CP) (LPP L LPQ) FP {!!} 
          LQ : HOD
          LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
          LQQ : LQ ⊆ Power Q
-         LQQ = ?
-
+         LQQ = {!!}
+-- S ⊆ ℕ