# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674270696 -32400
# Node ID 70bcb775115afe59b8b2565c79b9976fb6b3c4ba
# Parent  5e065f0a7ba28d38139522526fa3481145f983ab
...

diff -r 5e065f0a7ba2 -r 70bcb775115a src/Topology.agda
--- a/src/Topology.agda	Sat Jan 21 09:12:10 2023 +0900
+++ b/src/Topology.agda	Sat Jan 21 12:11:36 2023 +0900
@@ -481,6 +481,10 @@
 
 open import maximum-filter O
 
+CAP : (P : HOD) {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q)
+CAP P {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) *iso pqx
+... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) (sym *iso) px )
+
 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 with trio< (& P) o∅
@@ -489,7 +493,7 @@
    -- P is empty
    fip02 : {x : Ordinal } → ¬ odef P x
    fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) )
-... | tri> ¬a ¬b 0<P = record { limit = uf00 ; is-limit = {!!} } where
+... | tri> ¬a ¬b 0<P = record { limit = uf00 ; is-limit = uf01 } 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
@@ -497,6 +501,12 @@
         ; <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
+     nc : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → HOD
+     nc = ?
+     N∋nc :{X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → odef (N CSX fp) (& (nc CSX fp) )
+     N∋nc = ?
+     0<PP : o∅ o< & (Power P)
+     0<PP = ?
      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
@@ -522,15 +532,15 @@
                  → ⟪ 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 = ?
-     CAP : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q)
-     CAP {X} CSX fp {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) *iso pqx
-     ... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) (sym *iso) px )
      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)
+     maxf {X} CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 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)
          ( MaximumFilter.mf (maxf CSX fp) )
-         (F→ultra {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp)  ? ? (proper CSX fp)))
+         (F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)))
+     uf01 :  {X : Ordinal} (CX : * X ⊆ CS TP) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
+            {x : Ordinal} → odef (* X) x → odef (* x) (uf00 CX fip)
+     uf01 = ?
 
 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
@@ -541,32 +551,8 @@
      CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z)) 
      ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x
      ufl01 = ?
-     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 } = ?
-
-FilterProduct  : {P Q LP LQ : HOD } 
-     → (LPP : LP ⊆ Power P) (FP : Filter {LP} LPP)  
-     → (LPQ : LQ ⊆ Power Q) (FQ : Filter {LQ} LPQ)  
-     → Filter {ZFP LP LQ} ?
-FilterProduct  = ?
-
-FilterProj  : {P Q LPQ : HOD } 
-     → ( LPPQ : LPQ ⊆ Power (ZFP P Q))
-     → Filter {LPQ} LPPQ
-     → (Filter {Proj1 LPQ (Power P) (Power Q)} ?) ∧ (Filter {Proj2 LPQ (Power P) (Power Q)} ?) 
-FilterProj  = ?
-
-ProuctLimit→ProjLimit  : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  
-     → ( {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ)  (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) LPQ F UF )
-     → ( {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP)  (UF : ultra-filter F) → UFLP TP LP F UF) 
-     ∧ ( {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP)  (UF : ultra-filter F) → UFLP TQ LP F UF) 
-ProuctLimit→ProjLimit  = ?
-
-ProjLimit→ProductLimit  : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  
-     → ( {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP)  (UF : ultra-filter F) → UFLP TP LP F UF) 
-     ∧ ( {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP)  (UF : ultra-filter F) → UFLP TQ LP F UF) 
-     → {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ)  (UF : ultra-filter F) → UFLP (ProductTopology TP TQ) LPQ F UF
-ProjLimit→ProductLimit  = ?
+     ufl00 :  {v : Ordinal} → Neighbor TP (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ) v → filter F ⊆ * v
+     ufl00 {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; o⊆u = o⊆u } {x} fx = ?
 
 -- product topology of compact topology is compact