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

diff -r 6216562a2bce -r adba530ce1f0 src/OPair.agda
--- a/src/OPair.agda	Fri Jan 20 11:22:37 2023 +0900
+++ b/src/OPair.agda	Fri Jan 20 14:40:54 2023 +0900
@@ -254,12 +254,25 @@
 ZFPproj2 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
 ZFPproj2 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ2 (X⊆P px) )) 
 
-
+record PProj1 (L : HOD) (x : Ordinal) : Set n where 
+    field
+        pq : Ordinal
+        opq : ord-pair pq
+        Lpq : odef L pq    
+        x=pi1 : x ≡ pi1 opq
 
-
-
+-- LP' = Replace' L ( λ p lp → ZFPproj1 {P} {Q} {p} (λ {x} px → (LPQ lp _ (subst (λ k → odef k x) (sym *iso) px  ) )))           
 
-
+Proj1PP : (L P Q : HOD) → HOD
+Proj1PP L P Q = record { od = record { def = λ x → odef P x ∧ ((y : Ordinal) → PProj1 L y) } ; odmax = & P ; <odmax = odef∧< }
+   
+record PProj2 (L : HOD) (x : Ordinal) : Set n where 
+    field
+        pq : Ordinal
+        opq : ord-pair pq
+        Lpq : odef L pq    
+        x=pi2 : x ≡ pi2 opq
 
-
-
+Proj2PP : (L P Q : HOD) → HOD
+Proj2PP L P Q = record { od = record { def = λ x → odef Q x ∧ ((y : Ordinal) → PProj2 L y) } ; odmax = & Q ; <odmax = odef∧< }
+   
diff -r 6216562a2bce -r adba530ce1f0 src/Topology.agda
--- a/src/Topology.agda	Fri Jan 20 11:22:37 2023 +0900
+++ b/src/Topology.agda	Fri Jan 20 14:40:54 2023 +0900
@@ -410,16 +410,25 @@
 
 -- Ultra Filter has limit point
 
+record Neighbor {P : HOD} (TP : Topology P) (x v : Ordinal) : Set n where
+   field
+       u : Ordinal
+       ou : odef (OS TP) u
+       ux : odef (* u) x
+       v⊆P : * v ⊆ P
+       o⊆u : * u ⊆ * v
+
 record UFLP {P : HOD} (TP : Topology P) {L : HOD} (LP : L ⊆ Power P ) (F : Filter {L} {P} LP )
        (ultra : ultra-filter 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
+       is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ⊆ (* v)
 
 -- FIP is UFL
 
-record NFIP (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
+-- filter Base
+record FBase (P : HOD )(X : Ordinal ) (u : Ordinal) : Set n where
    field
        b x : Ordinal 
        b⊆X : * b ⊆ * X
@@ -435,10 +444,10 @@
      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 P X u } ; odmax = osuc (& P) 
-        ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (NFIP.u⊆P lt))  }
+     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  = NFIP.u⊆P nx xb
+     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
@@ -451,17 +460,17 @@
          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)
+              Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq)
+              xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq)
               sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
-              sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (NFIP.sb Np)) (sb⊆ case2 (NFIP.sb Nq)))
+              sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
               f20 : * (& Np+Nq) ⊆ * X
               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
+              ... | 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 
-                 → ⟪ subst (λ k → odef k w) *iso ( NFIP.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( NFIP.x⊆u Nq (proj2 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 = ?
      CAP : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q)
@@ -476,34 +485,37 @@
 
 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 = ?
+FIP→UFLP {P} TP fip {L} LP F UF = record { limit = FIP.limit fip ? ? ; P∋limit = ? ; is-limit = ? } where
+     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 } = ?
 
 -- 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) 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 : {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 {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
-    uflPQ : {L : HOD} → (LPQ : L ⊆ Power (ZFP P Q )) (F : Filter {L} LPQ)  (UF : ultra-filter F)
+     uflQ {L} LP F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) LP F UF
+     -- Product of UFL has limit point
+     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 = ?
+     uflPQ {L} LPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , {!!} >  ; P∋limit = {!!} ; is-limit = {!!} } where
+         LP : HOD  -- proj1 of LPQ
+         LP = Proj1PP L (Power P) (Power Q)
+         LPP : LP ⊆ Power P
+         LPP {x} ⟪ Px , p1 ⟫ = Px
+         FP : Filter {LP} {P} LPP
+         FP = record { filter = Proj1PP (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
+             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 = record { proper = ? ; ultra = ? }
          uflp : UFLP TP LPP FP UFP
-         uflp = ?
+         uflp = FIP→UFLP TP (Compact→FIP TP CP) LPP FP UFP