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

diff -r d20199031218 -r 2839815e7b50 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Wed Mar 08 17:36:15 2023 +0900
+++ b/src/Tychonoff.agda	Wed Mar 08 18:47:07 2023 +0900
@@ -505,9 +505,11 @@
              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
+                 a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw) 
+                 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw )
                  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 = ?
+                 ty70 = trans (cong₂ (λ j k → & < * j , k > ) (trans &iso (cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b ))))  refl ) (trans ?  (zp-iso (f⊆L F az _ zw ) ))
              ty71 : * z ⊆ ZFP (* x) Q
              ty71 = subst (λ k → * z ⊆ ZFP k Q) ty72 RxQ∋z where
                  ty72 : Rx ≡ * x