# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674181357 -32400
# Node ID 6216562a2bcefa494169e8d7ccfcc67ebad03405
# Parent  d6a8738ac505ae53db45bbdfc24b8a7bbea80456
...

diff -r d6a8738ac505 -r 6216562a2bce src/Topology.agda
--- a/src/Topology.agda	Thu Jan 19 17:22:02 2023 +0900
+++ b/src/Topology.agda	Fri Jan 20 11:22:37 2023 +0900
@@ -401,9 +401,8 @@
             fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w
             fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw
 
--- some day
-Compact→FIP : Set (suc n)
-Compact→FIP = {L : HOD} → (top : Topology L ) → Compact top  → FIP top
+Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
+Compact→FIP = ?
 
 -- existence of Ultra Filter
 
@@ -420,13 +419,12 @@
 
 -- FIP is UFL
 
-record NFIP {P : HOD} (TP : Topology P) {X : Ordinal } (LP : * X ⊆ CS TP ) (u : Ordinal) : Set n where
+record NFIP (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
    field
        b x : Ordinal 
        b⊆X : * b ⊆ * X
        sb  : Subbase (* b) x 
-       0<x : o∅ o< x
-       X∋u : odef (* X) u
+       u⊆P : * u ⊆ P
        x⊆u : * x ⊆ * u
 
 open import maximum-filter O
@@ -437,20 +435,22 @@
      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 → NFIP TP {X} CSX u } ; odmax = X 
-        ; <odmax = λ {x} lt → subst₂ (λ j k → j o< k) refl &iso (odef< (NFIP.X∋u lt))  }
-     N⊆PX : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → N CSX fp ⊆ * X
-     N⊆PX {X} CSX fp {z} nz = NFIP.X∋u nz
-     X⊆PP : {X : Ordinal } → (CSX : * X ⊆ CS TP) → * X ⊆ Power P
-     X⊆PP CSX lt = CS⊆PL TP (CSX lt)
-     F : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip CSX) → Filter {* X} {P} (X⊆PP CSX)
-     F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PX CSX fp ; filter1 = f1 ; filter2 = f2 } where
-         f1 :  {p q : HOD} → * X ∋ 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 ; 0<x = 0<x ; X∋u = Xp ; x⊆u = x⊆p } p⊆q = 
-                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; 0<x = 0<x ; X∋u = Xq ; x⊆u = λ {z} xp → 
-                            subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp)))  } 
-         f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → * X ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
-         f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; 0<x = f21 ; X∋u = Xpq ; x⊆u = f22 } where
+     N {X} CSX fp = record { od = record { def = λ u → NFIP P X u } ; odmax = osuc (& P) 
+        ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (NFIP.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  = NFIP.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 → 
+                            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  ))
+         f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
+         f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where
+              p∩q⊆p : * (& (p ∩ q)) ⊆ P
+              p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx ))
               Np+Nq = * (NFIP.b Np) ∪ * (NFIP.b Nq)
               xp∧xq = * (NFIP.x Np) ∩ * (NFIP.x Nq)
               sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
@@ -459,37 +459,51 @@
               f20 {x} npq with subst (λ k → odef k x) *iso npq
               ... | case1 np = NFIP.b⊆X Np np
               ... | case2 nq = NFIP.b⊆X Nq nq
-              f21 : o∅ o< & xp∧xq
-              f21 = fp f20 sbpq 
               f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
               f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq 
                  → ⟪ subst (λ k → odef k w) *iso ( NFIP.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( NFIP.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 } → * X ∋ p → * X ∋ q → * X ∋ (p ∩ q)
-     CAP = ?
-     maxf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (X⊆PP CSX) (F CSX fp)
-     maxf {X} CSX fp = F→Maximum (X⊆PP CSX) (CAP CSX fp) (F CSX fp) ? ? (proper CSX fp)
+     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)
      uf00 : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
-     uf00 {X} CSX fp = UFLP.limit ( uflp (X⊆PP CSX)
+     uf00 {X} CSX fp = UFLP.limit ( uflp (λ x → x) 
          ( MaximumFilter.mf (maxf CSX fp) )
-         (F→ultra (X⊆PP CSX) (CAP CSX fp) (F CSX fp)  ? ? (proper CSX fp)))
+         (F→ultra {Power P} {P} (λ x → x) (CAP CSX fp) (F CSX fp)  ? ? (proper CSX fp)))
 
--- some day
-FIP→UFLP : Set (suc (suc n))
-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 F ) → UFLP {P} TP {L} LP F UF
+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 = ?
 
 -- product topology of compact topology is compact
 
 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (ProductTopology TP TQ)
-Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflp ) where
+Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where
     L = pbase TP TQ
     LPQ = pbase⊆PL TP TQ
+    uflP : {L : HOD} → (LP : L ⊆ Power P) (F : Filter {L} LP)  (UF : ultra-filter F)
+             → UFLP TP LP F UF
+    uflP {L} LP F UF = FIP→UFLP TP (Compact→FIP TP CP) LP F UF
+    uflQ : {L : HOD} → (LP : L ⊆ Power Q) (F : Filter {L} LP)  (UF : ultra-filter F)
+             → UFLP TQ LP F UF
+    uflQ {L} LP F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) LP F UF
     -- Product of UFL has limit point
-    uflp : {L : HOD} → (LP : L ⊆ Power (ZFP P Q )) (F : Filter {L} LP)  (UF : ultra-filter F)
-             → UFLP (ProductTopology TP TQ) LP F UF
-    uflp {L} LP F UF = record { limit = & < ? , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} }
+    uflPQ : {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ)  (UF : ultra-filter F)
+             → UFLP (ProductTopology TP TQ) LPQ F UF
+    uflPQ {L} LPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} } where
+         LP : HOD
+         LP = ZFPproj1 (λ {x} p → LPQ ? _ p )
+         LPP : L ⊆ Power P
+         LPP = ?
+         FP : Filter ?
+         FP = ?
+         UFP : ultra-filter FP
+         UFP = ?
+         uflp : UFLP TP LPP FP UFP
+         uflp = ?
 
 
 
diff -r d6a8738ac505 -r 6216562a2bce src/filter.agda
--- a/src/filter.agda	Thu Jan 19 17:22:02 2023 +0900
+++ b/src/filter.agda	Fri Jan 20 11:22:37 2023 +0900
@@ -318,11 +318,3 @@
          (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fq) Lpq )
      ; proper  = subst₂ (λ j k → ¬ odef j k ) (sym *iso) ord-od∅ proper 
    }
-
--- all filter contains F
-F⊆X : { L P : HOD  } (LP : L ⊆ Power P) → Filter {L} {P} LP  → HOD
-F⊆X {L} {P} LP F = record { od = record { def = λ x → IsFilter {L} {P} LP x ∧ ( filter F ⊆ * x)  } ; odmax = osuc (& L)
-      ; <odmax = λ {x} lt → fx00 lt } where
-      fx00 : {x : Ordinal } → IsFilter LP x ∧ filter F ⊆ * x → x o< osuc (& L)
-      fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (IsFilter.f⊆L (proj1 lt ))  )
-
diff -r d6a8738ac505 -r 6216562a2bce src/maximum-filter.agda
--- a/src/maximum-filter.agda	Thu Jan 19 17:22:02 2023 +0900
+++ b/src/maximum-filter.agda	Fri Jan 20 11:22:37 2023 +0900
@@ -55,6 +55,14 @@
 import zorn 
 open zorn O _⊂_ PO
 
+
+-- all filter contains F                                                                              
+F⊆X : { L P : HOD  } (LP : L ⊆ Power P) → Filter {L} {P} LP  → HOD
+F⊆X {L} {P} LP F = record { od = record { def = λ x → IsFilter {L} {P} LP x ∧ ( filter F ⊆ * x)  } ; odmax = osuc (& L)
+      ; <odmax = λ {x} lt → fx00 lt } where                                                             
+      fx00 : {x : Ordinal } → IsFilter LP x ∧ filter F ⊆ * x → x o< osuc (& L)
+      fx00 {x} lt = subst (λ k → k o< osuc (& L)) &iso ( ⊆→o≤ (IsFilter.f⊆L (proj1 lt ))  )
+
 F→Maximum : {L P : HOD} (LP : L ⊆ Power P) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
       → (F : Filter {L} {P} LP) → o∅ o< & L →  {y : Ordinal } → odef (filter F) y →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP F
 F→Maximum {L} {P} LP CAP F 0<L {y} 0<F Fprop = record { mf = mf ; F⊆mf = subst (λ k → filter F ⊆ k ) (sym *iso) mf52