# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678257395 -32400
# Node ID faffe9a4bd0f22624151bf78f02489340b97c6a6
# Parent  5e6dfe739f6afdd5e8f2588acec02ba661ac7344
...

diff -r 5e6dfe739f6a -r faffe9a4bd0f src/Tychonoff.agda
--- a/src/Tychonoff.agda	Wed Mar 08 14:10:56 2023 +0900
+++ b/src/Tychonoff.agda	Wed Mar 08 15:36:35 2023 +0900
@@ -500,7 +500,19 @@
 
          --  FPSet is in Projection ⁻¹  F
          FPSet⊆F : {x : Ordinal } → odef FPSet x →  odef (filter F) (& (ZFP (* x) Q))
-         FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = ?
+         FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (filter F) k ) ty70 az where
+            ty70 : z ≡ & (ZFP (* x) Q)
+            ty70 = subst₂ ( λ j k → j ≡ k ) &iso refl (cong (&) (==→o≡ record { eq→  = ty71 ; eq← = ty74 } ) ) where
+               ty71 : {y : Ordinal } → odef (* z) y → odef (ZFP (* x) Q) y 
+               ty71 {y} zy = subst (λ k → ZFProduct (* x) Q k ) ty72 ( ab-pair ty73 aq ) where
+                  ty72 :  & < * ? , * (zπ2 is-apq) > ≡ y
+                  ty72 = ?
+                  ty73 : odef (* x) ?
+                  ty73 = subst (λ k → odef k ?) (trans (sym *iso) (sym (cong (*) x=ψz))) record {z = ? ; az = ? ; x=ψz = ? } 
+               ty74 : {y : Ordinal } → odef (ZFP (* x) Q) y  → odef (* z) y
+               ty74 {.(& < * _ , * _ >)} (ab-pair {a} {b} xx qy) with subst (λ k → odef k a) (sym (trans (sym *iso) (sym (cong (*) x=ψz)))) xx
+               ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = ?
+
 
          --  copy and pasted, sorry
          --