# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678027750 -32400
# Node ID 287d40830be583aa0491e53e55eb18c70f07cc8e
# Parent  6861b48c1e089d40364c5d99ce1c5b4fedc5e43b
...

diff -r 6861b48c1e08 -r 287d40830be5 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Sun Mar 05 20:07:24 2023 +0900
+++ b/src/Tychonoff.agda	Sun Mar 05 23:49:10 2023 +0900
@@ -341,35 +341,42 @@
          F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy)
          fx→px : {x : HOD } → filter F ∋ x → HOD 
          fx→px {x} fx = Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) ))
-         fx→px1 : {p : HOD } → (fp : filter F ∋  ZFP p Q ) → p ⊆  P  → fx→px fp ≡ p
-         fx→px1 {p} fp p⊆P = ==→o≡ record { eq→ = ? ; eq← = ? } where
+         fx→px1 : {p : HOD } {q : Ordinal } → odef Q q → (fp : filter F ∋  ZFP p Q ) → fx→px fp ≡ p
+         fx→px1 {p} {q} qq fp = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where
+             ty21 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >)))
+             ty21 pz qz = F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz ))  
+             ty32 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → zπ1 (ty21 pz qz) ≡ a
+             ty32 {a} {b} pz qz  = ty33 (ty21 pz qz) (cong (&) *iso) where
+                 ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
+                 ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
+                 ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c)
              ty20 : {x : Ordinal} → odef (fx→px fp) x → odef p x
-             ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = ? where
-                 ty22 : ZFProduct p Q (& < * a , * b >) 
-                 ty22 = ab-pair pz qz
+             ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef p k) a=x pz  where
                  ty24 : * x  ≡ * a 
                  ty24 = begin
-                  * x ≡⟨ cong (*) x=ψz ⟩
-                  _ ≡⟨ *iso  ⟩
-                  * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ proj1 (zp-iso1 {p} {Q} ? ) ⟩
-                  * a ∎ where open ≡-Reasoning
-                 ty23 : * (zπ1 ty22 ) ≡ * a
-                 ty23 = proj1 ( zp-iso1 {p} {Q} (ab-pair pz qz) )
-                 ty21 : odef (ZFP P Q ) (& (* (& ( < * a , * b > ) )))
-                 ty21 = F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz))
-                 a=x : x ≡ a
-                 a=x with subst (λ k → odef (ZFP P Q) k) &iso ty21 | subst (λ k → x ≡ k ) &iso x=ψz
-                 ... | t | refl with proj1 ( zp-iso1 {P} {Q} t )
-                 ... | u = subst₂ (λ j k → j ≡ k ) (trans &iso ?)  &iso (cong (&) u )
-                 pa : odef p x
-                 pa with subst (λ k → odef (ZFP P Q) k) &iso ty21 | subst (λ k → x ≡ k ) &iso x=ψz 
-                 ... | t | refl = ?
+                    * x ≡⟨ cong (*) x=ψz ⟩
+                    _ ≡⟨ *iso  ⟩
+                    * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair pz qz)))) ≡⟨ cong (*) (ty32 pz qz) ⟩
+                    * a ∎ where open ≡-Reasoning
+                 a=x : a  ≡ x 
+                 a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24))
+             ty22 : {x : Ordinal} → odef p x → odef (fx→px fp) x 
+             ty22 {x} px = record { z = _ ; az = ab-pair px qq ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) }  where
+                 ty12 : * x ≡ * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq ))))
+                 ty12 = begin
+                    * x ≡⟨ sym (cong (*) (ty32 px qq )) ⟩
+                    * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq )))) ∎ where open ≡-Reasoning
+                   
          FPSet : HOD
          FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )))
          FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋  ZFP q Q → FPSet ∋ q
-         FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = ? } where
-             ty11 : & q ≡ zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) ? )
-             ty11 = ?
+         FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where
+              ty10 : Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q
+              ty10 = begin
+                  Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡⟨ ? ⟩
+                  Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ 
+                  fx→px fq ≡⟨ fx→px1 ? fq  ⟩
+                  q ∎ where open ≡-Reasoning
          FPSet⊆PP :  FPSet  ⊆ Power P
          FPSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw
          ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } 
@@ -393,11 +400,20 @@
                   x⊆pxq : * x ⊆ ZFP p Q
                   x⊆pxq {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
                   ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where
+                      ty21 : ZFProduct P Q (& (* (& < * a , * b >)))
+                      ty21 = subst (λ k → ZFProduct P Q k) (cong & (sym *iso)) (ab-pair pw qw)  
+                      ty32 : ZFProduct P Q (& (* (& < * a , * b >)))
+                      ty32 = f⊆L F (subst (odef (filter F)) (sym &iso) fx)
+                            (& (* (& < * a , * b >))) (subst (λ k → odef k 
+                            (& (* (& < * a , * b >)))) (sym *iso) (subst (odef (* x)) (sym &iso) xw))
                       ty07 : odef (* x) (& < * a , * b >) 
                       ty07 = xw
                       ty08 : odef p a
                       ty08 = subst (λ k → odef k a ) (subst₂ (λ j k → j ≡ k) *iso *iso (sym (cong (*) x=ψz)))  
-                           record { z = _ ; az = xw ;  x=ψz = ? }
+                           record { z = _ ; az = xw ;  x=ψz = sym (trans &iso (ty33 ty32 (cong (&) *iso ))) } where
+                         ty33 : {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
+                         ty33 {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
+                         ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c)
                   ty05 : filter F ∋  ZFP p Q
                   ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) x⊆pxq
                   ty06 : ZFP p Q ⊆ ZFP q Q