# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1680672778 -32400
# Node ID 53a4bd63016a4d35ece38b4632e63b6732358b55
# Parent  c077532416d99c45856b346ddfa50c8b7c65a993
...

diff -r c077532416d9 -r 53a4bd63016a src/ZProduct.agda
--- a/src/ZProduct.agda	Wed Apr 05 09:00:53 2023 +0900
+++ b/src/ZProduct.agda	Wed Apr 05 14:32:58 2023 +0900
@@ -165,6 +165,7 @@
 ZPI1 : (A B : HOD) → HOD
 ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px )) 
 
+
 ZPI2 : (A B  : HOD) → HOD
 ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 px )) 
 
@@ -231,21 +232,43 @@
      ; fiso→ = λ x lt → refl
     }
 
+pj12 : (A B : HOD) {x : Ordinal} → (ab : odef (ZFP A B) x ) → 
+   (zπ1  (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ1 ab ))) ∧ 
+   (zπ2  (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ2 ab )))
+pj12 A B (ab-pair {x} {y} ax by) = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (prod-≡ pj24 ))) 
+      , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (prod-≡ pj24)))  ⟫ where
+   pj22 : odef (ZFP A B) (& (* (& < * x , * y >)))
+   pj22 = subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by)
+   pj23 : & < * (zπ1 pj22 ) , * (zπ2 pj22) > ≡ & (* (& < * x , * y >) )
+   pj23 = zp-iso pj22
+   pj24 : < * (zπ1 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) , * (zπ2 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) >
+    ≡ < * (& (* x)) ,  * (& (* y)) >
+   pj24 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ( trans pj23 (trans &iso 
+       (sym (cong (&) (cong₂ (λ j k → < j , k >) *iso *iso)) ))))
+pj02 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI2 A B) (zπ2 ab)
+pj02 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj2 (pj12 A B ab))) (sym &iso))  }
+pj01 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI1 A B) (zπ1 ab)
+pj01 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj1 (pj12 A B ab))) (sym &iso))  }
+pj2 :  (A B : HOD) (x : Ordinal) (lt : odef (ZFP A B) x) → odef (ZFP (ZPI2 A B) (ZPI1 A B)) (& < * (zπ2 lt) , * (zπ1 lt) >)
+pj2 A B x ab = ab-pair (pj02 A B x ab)  (pj01 A B x ab)
+aZPI1 : (A B : HOD) {y : Ordinal} → odef (ZPI1 A B) y → odef A y
+aZPI1 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef A k) (trans (
+    trans (sym &iso) (trans (sym (proj1 (pj12 A B az))) (sym &iso))) (sym x=ψz)  ) ( zp1 az )
+aZPI2 : (A B : HOD) {y : Ordinal} → odef (ZPI2 A B) y → odef B y
+aZPI2 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef B k) (trans (
+    trans (sym &iso) (trans (sym (proj2 (pj12 A B az))) (sym &iso))) (sym x=ψz)  ) ( zp2 az )
+pj1 :  (A B : HOD) (x : Ordinal) (lt : odef (ZFP (ZPI2 A B) (ZPI1 A B)) x) → odef (ZFP A B) (& < * (zπ2 lt) , * (zπ1 lt) >)
+pj1 A B _ (ab-pair ax by) = ab-pair (aZPI1 A B by) (aZPI2 A B ax) 
+
 ZFPsym : (A B  : HOD) → HODBijection (ZFP A B) (ZFP (ZPI2 A B) (ZPI1 A B))
 ZFPsym A B = record {
        fun←  = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) >
      ; fun→  = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) >
-     ; funB  = pj2
-     ; funA  = ?
+     ; funB  = pj2 A B
+     ; funA  = pj1 A B
      ; fiso← = λ xy ab → ?
-     ; fiso→ = λ xy ab → ?
-    } where
-       pj02 : (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI2 A B) (zπ2 ab)
-       pj02 x ab = record { z = _ ; az = ab ; x=ψz = ? }
-       pj2 :  (x : Ordinal) (lt : odef (ZFP A B) x) → odef (ZFP (ZPI2 A B) (ZPI1 A B)) (& < * (zπ2 lt) , * (zπ1 lt) >)
-       pj2 x ab = ab-pair (pj02 x ab) ? 
-       pj1 :  (x : Ordinal) (lt : odef (ZFP (ZPI2 A B) (ZPI1 A B)) x) → odef (ZFP A B) (& < * (zπ2 lt) , * (zπ1 lt) >)
-       pj1 _ (ab-pair {x} {y} record { z = z ; az = bz ; x=ψz = x=ψbz } ay) = ab-pair ? ?
+     ; fiso→ = λ xy ab → zp-iso ab
+    } 
 
 
 ZFP∩  : {A B C : HOD} → ( ZFP (A ∩ B) C ≡ ZFP A C ∩ ZFP B C ) ∧ ( ZFP C (A ∩ B) ≡ ZFP C A  ∩ ZFP C B )