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

diff -r faffe9a4bd0f -r d20199031218 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Wed Mar 08 15:36:35 2023 +0900
+++ b/src/Tychonoff.agda	Wed Mar 08 17:36:15 2023 +0900
@@ -500,19 +500,21 @@
 
          --  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 } = 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 } = ?
-
+         FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F ? (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where
+             Rx : HOD
+             Rx = Replace' (* z) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy)))
+             RxQ∋z : * z ⊆ ZFP Rx Q 
+             RxQ∋z {w} zw = subst (λ k → ZFProduct Rx Q k ) ty70 ( ab-pair record { z = w ; az = zw ; x=ψz = refl  } (zp2 (f⊆L F az _ zw ) ) ) where
+                 ty70 : & < * (& (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw))))) 
+                      , * (zπ2 (f⊆L F az w zw)) > ≡ w
+                 ty70 = ?
+             ty71 : * z ⊆ ZFP (* x) Q
+             ty71 = subst (λ k → * z ⊆ ZFP k Q) ty72 RxQ∋z where
+                 ty72 : Rx ≡ * x 
+                 ty72 = begin
+                    Rx ≡⟨ sym *iso ⟩
+                    * (& Rx)  ≡⟨ cong (*) (sym x=ψz ) ⟩
+                    * x ∎ where open ≡-Reasoning
 
          --  copy and pasted, sorry
          --