# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1680681932 -32400
# Node ID 2cbe0db250da24f1c582d247a70db141aadc0f76
# Parent  53a4bd63016a4d35ece38b4632e63b6732358b55
P x Q done

diff -r 53a4bd63016a -r 2cbe0db250da src/ZProduct.agda
--- a/src/ZProduct.agda	Wed Apr 05 14:32:58 2023 +0900
+++ b/src/ZProduct.agda	Wed Apr 05 17:05:32 2023 +0900
@@ -165,7 +165,6 @@
 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 )) 
 
@@ -260,16 +259,77 @@
 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 {
+ZPI1-iso : (A B : HOD) → {b : Ordinal } → odef B b → ZPI1 A B ≡ A
+ZPI1-iso P Q {q} qq = ==→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 = 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 (ZPI1 P Q) x → odef P x
+     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 (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 (ZPI1 P Q) 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 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair px qq )))
+         ty12 = begin
+            * x ≡⟨ sym (cong (*) (ty32 px qq )) ⟩
+            * (zπ1 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair px qq ))) ∎ where open ≡-Reasoning
+
+ZPI2-iso : (A B : HOD) → {b : Ordinal } → odef A b → ZPI2 A B ≡ B
+ZPI2-iso P Q {p} pp = ==→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 = subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz )
+     ty32 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → zπ2 (ty21 pz qz) ≡ b
+     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π2 p ≡ b
+         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 (&) b=d)
+     ty20 : {x : Ordinal} → odef (ZPI2 P Q) x → odef Q x
+     ty20 {x} record { z = _ ; az = ab-pair {a} {b} pz qz ; x=ψz = x=ψz } = subst (λ k → odef Q k) a=x qz  where
+         ty24 : * x  ≡ * b
+         ty24 = begin
+            * x ≡⟨ cong (*) x=ψz ⟩
+            _ ≡⟨ *iso  ⟩
+            * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pz qz))) ≡⟨ cong (*) (ty32 pz qz) ⟩
+            * b ∎ where open ≡-Reasoning
+         a=x : b  ≡ x
+         a=x = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (sym ty24))
+     ty22 : {x : Ordinal} → odef Q x → odef (ZPI2 P Q) x
+     ty22 {x} qx = record { z = _ ; az = ab-pair pp qx  ; x=ψz = subst₂ (λ j k → j ≡ k) &iso refl (cong (&) ty12 ) }  where
+         ty12 : * x ≡ * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx)))
+         ty12 = begin
+            * x ≡⟨ sym (cong (*) (ty32 pp qx  )) ⟩
+            * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx  ))) ∎ where open ≡-Reasoning
+
+
+ZFPsym1 : (A B  : HOD) → HODBijection (ZFP A B) (ZFP (ZPI2 A B) (ZPI1 A B))
+ZFPsym1 A B = record {
        fun←  = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) >
      ; fun→  = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) >
      ; funB  = pj2 A B
      ; funA  = pj1 A B
-     ; fiso← = λ xy ab → ?
+     ; fiso← = λ xy ab → pj00 A B ab
      ; fiso→ = λ xy ab → zp-iso ab
-    } 
+    } where
+       pj10 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) 
+           → & < * (zπ1 ab) , * (zπ2 ab) > ≡ & < *  (zπ2 (pj1 A B xy ab)) ,  * (zπ1 (pj1 A B xy ab)) >
+       pj10 A B {.(& < * _ , * _ >)} (ab-pair ax by ) = refl
+       pj00 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) 
+           → & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) > ≡ xy 
+       pj00 A B {xy} ab = trans (sym (pj10 A B ab)) (zp-iso {ZPI2 A B} {ZPI1 A B} {xy} ab)
 
+ZFPsym : (A B  : HOD) → {a b : Ordinal } → odef A a → odef B b  → HODBijection (ZFP A B) (ZFP B A)
+ZFPsym A B aa bb = subst₂ ( λ j k → HODBijection (ZFP A B) (ZFP j k)) (ZPI2-iso A B aa) (ZPI1-iso A B bb) ( ZFPsym1 A B )
 
 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 )
 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00  ; eq← = zfp01 } where