# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1672278843 -32400
# Node ID a9a7ad7784cce6542c9149ffefa55836af040ca5
# Parent  7ce2cc622c92e4e4388715363b16cf2b1f53265e
fix topology

diff -r 7ce2cc622c92 -r a9a7ad7784cc src/Topology.agda
--- a/src/Topology.agda	Wed Dec 28 18:14:29 2022 +0900
+++ b/src/Topology.agda	Thu Dec 29 10:54:03 2022 +0900
@@ -30,7 +30,7 @@
 import ODC
 open ODC O
 
-open import filter
+open import filter O
 open import OPair O
 
 
@@ -78,10 +78,10 @@
    fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
    fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
 
-record FIP {L : HOD} (top : Topology L)  ( P : HOD ) : Set (suc n) where
+record FIP {L : HOD} (top : Topology L) : Set (suc n) where
    field
-       fipS⊆PL :  P ⊆ CS top
-       fip≠φ : { x : HOD } → Finite-∩ P x → ¬ ( x ≡ od∅ )
+       fipS⊆PL :  L ⊆ CS top
+       fip≠φ : { x : HOD } → Finite-∩ L x → ¬ ( x ≡ od∅ )
 
 -- Compact
 
@@ -89,24 +89,40 @@
    fin-e : {x : HOD} → S ∋ x → Finite-∪ S x
    fin-∪  : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
 
-record Compact  {L : HOD} (top : Topology L) ( P : HOD ) : Set (suc n) where
+record Compact  {L : HOD} (top : Topology L)  : Set (suc n) where
    field
-       finCover        : {X : HOD} → X ⊆ OS top → X covers P → HOD
-       isFinCover      : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → (finCover xo xcp ) covers P
-       isFiniteCover   : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → Finite-∪ X (finCover xo xcp  )
+       finCover  : {X : HOD} → X ⊆ OS top → X covers L → HOD
+       isCover   : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → (finCover xo xcp ) covers L
+       isFinite  : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers L ) → Finite-∪ X (finCover xo xcp  )
 
 -- FIP is Compact
 
-FIP→Compact : {L P : HOD} → (top : Topology L ) → FIP top P → Compact top P
-FIP→Compact {L} {P} TL fip = record { finCover = ? ; isFinCover = ? ; isFiniteCover = ? }
+FIP→Compact : {L : HOD} → (top : Topology L ) → FIP top  → Compact top 
+FIP→Compact {L} TL fip = record { finCover = ? ; isCover = ? ; isFinite = ? }
 
-Compact→FIP : {L P : HOD} → (top : Topology L ) → Compact top P → FIP top P
+Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top 
 Compact→FIP = {!!}
 
 -- Product Topology
 
 open ZFProduct 
 
+record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
+   field
+       p : Ordinal
+       q : Ordinal
+       op : odef (OS TP) p
+       qq : odef Q q
+       prod : x ≡ & < * p , * q >
+
+record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
+   field
+       p : Ordinal
+       q : Ordinal
+       oq : odef (OS TQ) q
+       pp : odef P p
+       prod : x ≡ & < * p , * q >
+
 _Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
 _Top⊗_ {P} {Q} TP TQ = record {
        OS    = POS
@@ -114,16 +130,48 @@
     ;  o∪ = ?
     ;  o∩ = ?
   } where
-      box : HOD
-      box = ZFP (OS TP) (OS TQ) 
-      POS : HOD
-      POS = ?
+        box : HOD
+        box = ZFP (OS TP) (OS TQ) 
+        --  B : (OS P ∋ x →  proj⁻¹ x ) ∨ (OS Q ∋ y  →  proj⁻¹ y )
+        --  U ⊂ ZFP P Q  ∧ ( U ∋ ∀ x → B ∋ ∃ b → b ∋ x ∧  b ⊂ U )
+        base : HOD
+        base = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (ZFP P Q) ; <odmax = ? }
+        POS : HOD
+        POS = record { od = record { def = λ x → {b : Ordinal } → odef (Power base) b ∧ odef (Union (* b)) x } 
+            ; odmax = & (ZFP P Q) ; <odmax = ? }
 
 -- existence of Ultra Filter 
 
+open Filter 
+
 -- Ultra Filter has limit point
 
+record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  (uf : ultra-filter {L} {P} {LP} F) : Set (suc (suc n)) where
+   field
+       limit : Ordinal
+       P∋limit : odef P limit
+       is-limit : {o : Ordinal} → odef (OS TP) o → odef (* o) limit → (* o) ⊆ filter F
+
 -- FIP is UFL
 
+FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP 
+   →  {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf 
+FIP→UFLP {P} TP fip {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? }
+
+UFLP→FIP : {P : HOD} (TP : Topology P) → 
+   ( {L : HOD} (LP : L ⊆ Power P ) (F : Filter LP )  (uf : ultra-filter {L} {P} {LP} F) → UFLP TP LP F uf ) → FIP TP 
+UFLP→FIP {P} TP uflp = record { fipS⊆PL = ? ; fip≠φ = ? }
+
 -- Product of UFL has limit point (Tychonoff)
 
+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
+    uflp : {L : HOD} (LP : L ⊆ Power (ZFP P Q)) (F : Filter LP)
+            (uf : ultra-filter {L} {_} {LP} F) → UFLP (TP Top⊗ TQ) LP F uf
+    uflp {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? }
+
+
+
+
+
+