# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674351532 -32400
# Node ID 46dc298bdd77aa3d875d8180d5d0a5c751697497
# Parent  938ada7fd66c98be9fb18986b4e013d335bd0c37
...

diff -r 938ada7fd66c -r 46dc298bdd77 src/OPair.agda
--- a/src/OPair.agda	Sat Jan 21 20:20:43 2023 +0900
+++ b/src/OPair.agda	Sun Jan 22 10:38:52 2023 +0900
@@ -146,25 +146,6 @@
 p-pi2 :  { x y : HOD } → (p : def ZFPair (&  < x , y >) ) →  π2 p ≡ y
 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
-ω-pair :  {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & (x , y) o< next m
-ω-pair lx ly = next< (omax<nx lx ly ) ho<
-
-ω-opair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & < x , y > o< next m
-ω-opair {x} {y} {m} lx ly = lemma0 where
-    lemma0 : & < x , y > o< next m
-    lemma0 = osucprev (begin
-         osuc (& < x , y >)
-       <⟨ osuc<nx ho< ⟩
-         next (omax (& (x , x)) (& (x , y)))
-       ≡⟨ cong (λ k → next k) (sym ( omax≤ _ _ pair-xx<xy )) ⟩
-         next (osuc (& (x , y)))
-       ≡⟨ sym (nexto≡) ⟩
-         next (& (x , y))
-       ≤⟨ x<ny→≤next (ω-pair lx ly) ⟩
-         next m
-       ∎ ) where
-          open o≤-Reasoning O
-
 _⊗_ : (A B : HOD) → HOD
 A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
@@ -194,20 +175,10 @@
 
 ZFP  : (A B : HOD) → HOD
 ZFP  A B = record { od = record { def = λ x → ZFProduct A B x  } 
-        ; odmax = omax (next (odmax A)) (next (odmax B)) ; <odmax = λ {y} px → lemma y px }  -- this is too large
+        ; odmax = odmax ( A ⊗ B ) ; <odmax = λ {y} px → <odmax ( A ⊗ B ) (lemma0 px) }  
    where
-       lemma : (y : Ordinal) → ZFProduct A B y → y o< omax (next (odmax A)) (next (odmax B))
-       lemma p ( ab-pair {x} {y} ax by ) with trio< (& A) (& B) 
-       lemma p ( ab-pair {x} {y} ax by ) | tri< a ¬b ¬c = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym &iso)
-            ax ))  (lemma1 by )) (omax-y _ _ ) where
-               lemma1 : odef B y → & (* y) o< next (HOD.odmax B)
-               lemma1 lt = x<nextA {B} (d→∋ B lt)
-       lemma p ( ab-pair {x} {y} ax by ) | tri≈ ¬a b ¬c = ordtrans (ω-opair (x<nextA {A} 
-          (d→∋ A ax)) lemma2 ) (omax-x _ _ ) where
-                lemma2 :  & (* y) o< next (HOD.odmax A)
-                lemma2 = ordtrans ( subst (λ k → & (* y) o< k ) (sym b) (c<→o< (d→∋ B by))) ho<
-       lemma p ( ab-pair {x} {y} ax by ) | tri> ¬a ¬b c = ordtrans (ω-opair  (x<nextA {A} (d→∋ A ax ))
-           (A<Bnext c (subst (λ k → odef B k ) (sym &iso) by))) (omax-x _ _ ) 
+        lemma0 :  {A B : HOD} {x : Ordinal} → ZFProduct A B x → odef (A ⊗ B) x
+        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
 
 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ZFP A B ∋ < a , b >
 ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb ) 
@@ -266,7 +237,7 @@
 -- LP' = Replace' L ( λ p lp → ZFPproj1 {P} {Q} {p} (λ {x} px → (LPQ lp _ (subst (λ k → odef k x) (sym *iso) px  ) )))           
 
 Proj1 : (L P Q : HOD) → HOD
-Proj1 L P Q = record { od = record { def = λ x → odef P x ∧ ((y : Ordinal) → ZProj1 L y) } ; odmax = & P ; <odmax = odef∧< }
+Proj1 L P Q = record { od = record { def = λ x → odef P x ∧ ZProj1 L x } ; odmax = & P ; <odmax = odef∧< }
    
 record ZProj2 (L : HOD) (x : Ordinal) : Set n where 
     field
@@ -276,5 +247,5 @@
         x=pi2 : x ≡ pi2 opq
 
 Proj2 : (L P Q : HOD) → HOD
-Proj2 L P Q = record { od = record { def = λ x → odef Q x ∧ ((y : Ordinal) → ZProj2 L y) } ; odmax = & Q ; <odmax = odef∧< }
+Proj2 L P Q = record { od = record { def = λ x → odef Q x ∧ ZProj2 L x } ; odmax = & Q ; <odmax = odef∧< }
    
diff -r 938ada7fd66c -r 46dc298bdd77 src/Topology.agda
--- a/src/Topology.agda	Sat Jan 21 20:20:43 2023 +0900
+++ b/src/Topology.agda	Sun Jan 22 10:38:52 2023 +0900
@@ -461,15 +461,18 @@
        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 )
+record UFLP {P : HOD} (TP : Topology P)  (F : Filter {Power P} {P} (λ x → x) )
        (ultra : ultra-filter F ) : Set (suc (suc n)) where
    field
        limit : Ordinal
        P∋limit : odef P limit
        is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ⊆ (* v)
 
+--
+-- Neighbor on x is a Filter (on Power P)
+--
 NeighborF : {P : HOD} (TP : Topology P)  (x : Ordinal ) → Filter {Power P} {P} (λ x → x) 
-NeighborF {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = f1 ; filter2 = ? } where
+NeighborF {P} TP x = record { filter = NF ; f⊆L = NF⊆PP ; filter1 = f1 ; filter2 = f2 } where
     nf00 : {v : Ordinal } → Neighbor TP x v → odef (Power P) v
     nf00 {v} nei y vy = Neighbor.v⊆P nei vy
     NF : HOD
@@ -491,6 +494,7 @@
          f20 : * upq ⊆ * (& (p ∩ q))
          f20 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) ( λ {x} pq 
            → ⟪ subst (λ k → odef k x) *iso (Neighbor.o⊆u Np (proj1 pq))  , subst (λ k → odef k x) *iso (Neighbor.o⊆u Nq (proj2 pq)) ⟫  )
+
 -- FIP is UFL
 
 -- filter Base
@@ -509,7 +513,7 @@
 ... | ⟪ 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
+   ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP
 UFLP→FIP {P} TP uflp with trio< (& P) o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = {!!} } where
@@ -557,70 +561,60 @@
      proper = ?
      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 P)  (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp)
+     ultraf : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( MaximumFilter.mf (maxf CSX fp))
+     ultraf {X} CSX fp = F→ultra {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 P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp)))
+     uf00 {X} CSX fp = UFLP.limit ( uflp ( MaximumFilter.mf (maxf CSX fp) ) (ultraf CSX fp))
      uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
             {x : Ordinal} → odef (* X) x → odef (* x) (uf00 CSX fip)
-     uf01 {X} CSX fp {x} xx = UFLP.is-limit ( uflp (λ x → x)
-         ( MaximumFilter.mf (maxf CSX fp) )
-         (F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc CSX fp) (proper CSX fp))) 
-            record { u = ? ; ou = ? ; ux = ? ; v⊆P = ? ; o⊆u = ? } ?
+     uf01 {X} CSX fp {x} xx = UFLP.is-limit ( uflp  ( MaximumFilter.mf (maxf CSX fp) ) (ultraf CSX fp)) ? ?
+            
 
 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 {P} TP fip {L} LP F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where
+   →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
+FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 ; P∋limit = ? ; is-limit = ufl00 } where
      CF : HOD
      CF = Replace' (filter F) (λ x fx → Cl TP x  )
      CF⊆CS : CF ⊆ CS TP
      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 = ?
+     ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 )
+     ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01  
      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 = ?
+     ufl00 {v} nei {x} fx = ?
 
 -- 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
-     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
+     uflP : (F : Filter {Power P} {P} (λ x → x))  (UF : ultra-filter F)
+             → UFLP TP F UF
+     uflP F UF = FIP→UFLP TP (Compact→FIP TP CP) F UF
+     uflQ : (F : Filter {Power Q} {Q} (λ x → x))  (UF : ultra-filter F)
+             → UFLP TQ F UF
+     uflQ F UF = FIP→UFLP TQ (Compact→FIP TQ CQ) 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 ) , * ( UFLP.limit uflq ) >  ; P∋limit = Pf ; is-limit = isL } where
-         LP : HOD  -- proj1 of LPQ
-         LP = Proj1 L (Power P) (Power Q)
-         LPP : LP ⊆ Power P
-         LPP {x} ⟪ Px , p1 ⟫ = Px
-         FP : Filter {LP} {P} LPP
+     uflPQ :  (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
+             → UFLP (ProductTopology TP TQ) F UF
+     uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) >  ; P∋limit = Pf ; is-limit = isL } where
+         FP : Filter {Power P} {P} (λ x → x)
          FP = record { filter = Proj1 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
-             ty00 :  Proj1 (filter F) (Power P) (Power Q) ⊆ LP
-             ty00 {x} ⟪ PPx , ppf ⟫ = ⟪ PPx , ( λ y → record { pq = ZProj1.pq (ppf y)
-                 ; opq = ZProj1.opq (ppf y) ; Lpq = f⊆L F (ZProj1.Lpq (ppf y)) ; x=pi1 = ZProj1.x=pi1 (ppf y) } )  ⟫
+             ty00 :  Proj1 (filter F) (Power P) (Power Q) ⊆ Power P
+             ty00 {x} ⟪ PPx , ppf ⟫ = PPx
          UFP : ultra-filter FP
          UFP = record { proper = ? ; ultra = ? }
-         uflp : UFLP TP LPP FP UFP
-         uflp = FIP→UFLP TP (Compact→FIP TP CP) LPP FP UFP
+         uflp : UFLP TP FP UFP
+         uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
 
-         LQ : HOD  -- proj1 of LPQ
-         LQ = Proj2 L (Power P) (Power Q)
-         LQP : LQ ⊆ Power Q
-         LQP {x} ⟪ Qx , q1 ⟫ = Qx
-         FQ : Filter {LQ} {Q} LQP
+         FQ : Filter {Power Q} {Q} (λ x → x)
          FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = ? ; filter2 = ? } where
-             ty00 :  Proj2 (filter F) (Power P) (Power Q) ⊆ LQ
-             ty00 {x} ⟪ QPx , ppf ⟫ = ⟪ QPx , ( λ y → record { pq = ZProj2.pq (ppf y)
-                 ; opq = ZProj2.opq (ppf y) ; Lpq = f⊆L F (ZProj2.Lpq (ppf y)) ; x=pi2 = ZProj2.x=pi2 (ppf y) } )  ⟫
+             ty00 :  Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q
+             ty00 {x} ⟪ QPx , ppf ⟫ = QPx
          UFQ : ultra-filter FQ
          UFQ = record { proper = ? ; ultra = ? }
-         uflq : UFLP TQ LQP FQ UFQ
-         uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) LQP FQ UFQ
+         uflq : UFLP TQ FQ UFQ
+         uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ
 
          Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
          Pf = ?