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

diff -r 2839815e7b50 -r 61fc99e65055 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Wed Mar 08 18:47:07 2023 +0900
+++ b/src/Tychonoff.agda	Wed Mar 08 19:52:41 2023 +0900
@@ -500,16 +500,22 @@
 
          --  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 } = filter1 F ? (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where
+         FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F ty80 (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
                  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 )
+                 ty71 : & (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)))) 
+                     ≡ zπ1 (subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw ))  
+                 ty71 = begin
+                     & (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)))) ≡⟨ &iso ⟩ 
+                     zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)) ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ 
+                     zπ1 (subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw ))  ∎ where open ≡-Reasoning
                  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 = 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 ) ))
+                 ty70 = trans (cong₂ (λ j k → & < * j , k > ) ? refl )  (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 
@@ -517,6 +523,12 @@
                     Rx ≡⟨ sym *iso ⟩
                     * (& Rx)  ≡⟨ cong (*) (sym x=ψz ) ⟩
                     * x ∎ where open ≡-Reasoning
+             ty80 : Power (ZFP P Q) ∋ ZFP (* x) Q
+             ty80 y yx = isP→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where
+                 ty81 : * x ⊆ P 
+                 ty81 {w} xw with subst (λ k → odef k w) (trans (cong (*) x=ψz ) *iso ) xw
+                 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (trans (sym &iso) (sym x=ψz1)) ?
+                     -- ( zp1 (f⊆L F az _ ? ) )
 
          --  copy and pasted, sorry
          --