# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678298236 -32400
# Node ID 59e927672b807e44e1cf6903ba3896127eb16778
# Parent  d2506e861dbf62c3e41daa6b5aae41a1035fd99a
Tyconoff done

diff -r d2506e861dbf -r 59e927672b80 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Thu Mar 09 02:31:41 2023 +0900
+++ b/src/Tychonoff.agda	Thu Mar 09 02:57:16 2023 +0900
@@ -681,7 +681,44 @@
 
          --  FQSet is in Projection ⁻¹  F
          FQSet⊆F : {x : Ordinal } → odef FQSet x →  odef (filter F) (& (ZFP P (* x) ))
-         FQSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = ?
+         FQSet⊆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π2 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy)))
+             PxRx∋z : * z ⊆ ZFP P Rx  
+             PxRx∋z {w} zw = subst (λ k → ZFProduct P Rx k ) ty70 ( ab-pair (zp1 b) record { z = w ; az = zw ; x=ψz = refl } ) 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 )
+                 ty73 : & (* (zπ2 a)) ≡ zπ2 b 
+                 ty73 = begin
+                     & (* (zπ2 a)) ≡⟨ &iso ⟩ 
+                     zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ 
+                     zπ2 b ∎  where open ≡-Reasoning
+                 ty70 : & < * (zπ1 b) , * (& (* (zπ2 a)))  > ≡ w
+                 ty70 with zp-iso (subst (λ k → odef (ZFP P Q) k) (sym &iso) (f⊆L F az _ zw )) 
+                 ... | eq = trans (cong₂ (λ j k → & < j , * k > ) refl ty73 ) (trans eq &iso ) 
+             ty71 : * z ⊆ ZFP P (* x) 
+             ty71 = subst (λ k → * z ⊆ ZFP P k ) ty72 PxRx∋z where
+                 ty72 : Rx ≡ * x 
+                 ty72 = begin
+                    Rx ≡⟨ sym *iso ⟩
+                    * (& Rx)  ≡⟨ cong (*) (sym x=ψz ) ⟩
+                    * x ∎ where open ≡-Reasoning
+             ty80 : Power (ZFP P Q) ∋ ZFP P (* x) 
+             ty80 y yx = isQ→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where
+                 ty81 : * x ⊆ Q 
+                 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 Q k) (sym ty84) ty87 where
+                      a =  f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1)) 
+                                 (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1))
+                      b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) (f⊆L F az _ az1 )
+                      ty87 : odef Q (zπ2 b)
+                      ty87 = zp2 b
+                      ty84 : w ≡ (zπ2 b)
+                      ty84 = begin
+                       w ≡⟨ trans x=ψz1 &iso ⟩
+                       zπ2 a ≡⟨ cong zπ2 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b )) ⟩
+                       zπ2 b  ∎ where open ≡-Reasoning
+
 
          uflq : UFLP TQ FQ UFQ
          uflq = FIP→UFLP TQ (Compact→FIP TQ CQ) FQ UFQ