# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1672401554 -32400
# Node ID fabcb7d9f50c4a6990543194affcda55be8b68d8
# Parent  81b859b678a8a4ce2373a197bd0fd23b6b8ebfa4
...

diff -r 81b859b678a8 -r fabcb7d9f50c src/OPair.agda
--- a/src/OPair.agda	Thu Dec 29 14:42:28 2022 +0900
+++ b/src/OPair.agda	Fri Dec 30 20:59:14 2022 +0900
@@ -248,6 +248,18 @@
        zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
        ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba) 
 
+ZFPproj1 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
+ZFPproj1 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ1 (X⊆P px) )) 
+
+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) )) 
 
 
 
+
+
+
+
+
+
+
diff -r 81b859b678a8 -r fabcb7d9f50c src/Topology.agda
--- a/src/Topology.agda	Thu Dec 29 14:42:28 2022 +0900
+++ b/src/Topology.agda	Fri Dec 30 20:59:14 2022 +0900
@@ -162,32 +162,26 @@
     uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ)
             (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf
     uflp {L} LPQ F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } where
-         lprod : {x y : Ordinal } → (ly : odef L y) → odef (ZFP P Q) x
-         lprod {x} {y} ly = LPQ ly x ?
-         -- LP : HOD  
-         -- LP = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
          LP : HOD  
-         LP = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→P ly ) }
-          ; odmax = & P ; <odmax = ? }   where
-            L→P : {y : Ordinal } → odef L y → HOD
-            L→P {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ1 (LPQ ly z yz )  ≡ x } 
-               ; odmax = & P ; <odmax = ? }
+         LP = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
          LPP : LP ⊆ Power P
-         LPP = ?
+         LPP record { z = z ; az = az ; x=ψz = x=ψz } w xw = tp02 (subst (λ k → odef k w) 
+           (subst₂ (λ j k → j ≡ k) refl *iso (cong (*) x=ψz) )  xw) where
+             tp02 : Replace' (* z) (λ z₁ xz → * (zπ1 (LPQ (subst (odef L) (sym &iso) az) (& z₁) (subst (λ k → odef k (& z₁)) (sym *iso) xz)))) ⊆ P
+             tp02 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k ) (trans (sym &iso) (sym x=ψz1)  ) 
+                  (zp1 (LPQ (subst (λ k → odef L k) (sym &iso) az) _ (tp03 az1 ))) where
+                    tp03 : odef (* z) z1 →  odef (* (& (* z))) (& (* z1)) 
+                    tp03 lt = subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) lt)
          FP : Filter LPP
          FP = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
          uFP : ultra-filter FP
          uFP = record { proper = ? ; ultra = ? }
          LQ : HOD  
-         LQ = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→Q ly ) }
-          ; odmax = & P ; <odmax = ? }   where
-            L→Q : {y : Ordinal } → odef L y → HOD
-            L→Q {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ2 (LPQ ly z yz )  ≡ x } 
-               ; odmax = & Q ; <odmax = ? }
+         LQ = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ2 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
          LQQ : LQ ⊆ Power Q
          LQQ = ?
          uflpp : UFLP {P} TP {LP} LPP FP uFP
-         uflpp = ?
+         uflpp = record { limit = ? ; P∋limit = ? ; is-limit = ? }