--- a/src/OPair.agda	Sun Mar 05 14:46:53 2023 +0900
+++ b/src/OPair.agda	Sun Mar 05 20:07:24 2023 +0900
@@ -198,6 +198,11 @@
 zp-iso :  { A B : HOD } → {x : Ordinal } → (p : odef (ZFP A B) x ) → & < * (zπ1 p) , * (zπ2 p) > ≡ x
 zp-iso {A} {B} {_} (ab-pair {a} {b} aa bb)  = refl
 
+zp-iso1 :  { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (* (zπ1 p) ≡ (* a)) ∧ (* (zπ2 p) ≡ (* b))
+zp-iso1 {A} {B} {a} {b} pab = prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) zz11) ) where
+      zz11 : & < * (zπ1 pab) , * (zπ2 pab) > ≡ & < * a , * b >
+      zz11 = zp-iso pab
+
 ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
 ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
 

--- a/src/Tychonoff.agda	Sun Mar 05 14:46:53 2023 +0900
+++ b/src/Tychonoff.agda	Sun Mar 05 20:07:24 2023 +0900
@@ -339,15 +339,37 @@
          isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q
          F⊆pxq : {x : HOD } → filter F ∋ x →  x ⊆ ZFP P Q
          F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy)
+         fx→px : {x : HOD } → filter F ∋ x → HOD 
+         fx→px {x} fx = Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) ))
+         fx→px1 : {p : HOD } → (fp : filter F ∋  ZFP p Q ) → p ⊆  P  → fx→px fp ≡ p
+         fx→px1 {p} fp p⊆P = ==→o≡ record { eq→ = ? ; eq← = ? } where
+             ty20 : {x : Ordinal} → odef (fx→px fp) x → odef p x
+             ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = ? where
+                 ty22 : ZFProduct p Q (& < * a , * b >) 
+                 ty22 = ab-pair pz qz
+                 ty24 : * x  ≡ * a 
+                 ty24 = begin
+                  * x ≡⟨ cong (*) x=ψz ⟩
+                  _ ≡⟨ *iso  ⟩
+                  * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ proj1 (zp-iso1 {p} {Q} ? ) ⟩
+                  * a ∎ where open ≡-Reasoning
+                 ty23 : * (zπ1 ty22 ) ≡ * a
+                 ty23 = proj1 ( zp-iso1 {p} {Q} (ab-pair pz qz) )
+                 ty21 : odef (ZFP P Q ) (& (* (& ( < * a , * b > ) )))
+                 ty21 = F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz))
+                 a=x : x ≡ a
+                 a=x with subst (λ k → odef (ZFP P Q) k) &iso ty21 | subst (λ k → x ≡ k ) &iso x=ψz
+                 ... | t | refl with proj1 ( zp-iso1 {P} {Q} t )
+                 ... | u = subst₂ (λ j k → j ≡ k ) (trans &iso ?)  &iso (cong (&) u )
+                 pa : odef p x
+                 pa with subst (λ k → odef (ZFP P Q) k) &iso ty21 | subst (λ k → x ≡ k ) &iso x=ψz 
+                 ... | t | refl = ?
          FPSet : HOD
          FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )))
          FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋  ZFP q Q → FPSet ∋ q
-         FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = ? ; x=ψz = ? } where
-             ty04 : q ≡ Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq ) xy)))
-             ty04 = ==→o≡ record { eq→ = ? ; eq← = ? } where
-                ty041 : {x : Ordinal} → odef q x → odef (Replace' (* (& (ZFP q Q)))
-                  (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy)))) x
-                ty041 {x} qx = record { z = _ ; az = subst (λ k → odef k (& < * x , * ? > )) (sym *iso) (ab-pair qx ? )  ;  x=ψz = ? }
+         FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = ? } where
+             ty11 : & q ≡ zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) ? )
+             ty11 = ?
          FPSet⊆PP :  FPSet  ⊆ Power P
          FPSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw
          ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 }