# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1680649789 -32400
# Node ID e7743ac5a070aed6ef11e2909ef21a660cda6e59
# Parent  b15dd4438d504d783e9a07680e48af9f99df595a
OrdBijection (& (ZFP A B)) (& (ZFP B A))

diff -r b15dd4438d50 -r e7743ac5a070 src/ZProduct.agda
--- a/src/ZProduct.agda	Mon Apr 03 15:02:36 2023 +0900
+++ b/src/ZProduct.agda	Wed Apr 05 08:09:49 2023 +0900
@@ -233,22 +233,26 @@
 
 ZFPsym : (A B  : HOD) → OrdBijection (& (ZFP A B)) (& (ZFP B A))
 ZFPsym A B = record {
-       fun←  = λ xy ab → & < * (zπ2 (subst (λ k → odef k xy) *iso ab)) , * (zπ1 (subst (λ k → odef k xy) *iso ab)) > 
-     ; fun→  = λ xy ba → & < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) > 
-     ; funB  = λ xy ab → subst (λ k → odef k (&
-             < * (zπ2 (subst (λ k → odef k xy) *iso ab)) , * (zπ1 (subst (λ k → odef k xy) *iso ab)) >)) 
-          (sym *iso) ( ab-pair (zp2 (subst (λ k → odef k xy) *iso ab)) (zp1 (subst (λ k → odef k xy) *iso ab))  )
-     ; funA  = λ xy ba → subst (λ k → odef k (&
-             < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) >)) 
-          (sym *iso) ( ab-pair (zp2 (subst (λ k → odef k xy) *iso ba)) (zp1 (subst (λ k → odef k xy) *iso ba))  )
-     ; fiso← = λ xy ba → trans (cong₂ (λ j k → & < * j , * k > ) (proj2 (zp-iso0 {A} {B} {zπ2 (subst (λ k → odef k xy) *iso ba)} {zπ1 (subst (λ k → odef k xy) *iso ba)} (lemma1 ba) )) 
-       ? ) ( zp-iso (subst (λ k → odef k xy) *iso ba )) 
-     ; fiso→ = λ xy ab → trans (cong₂ (λ j k → & < * j , * k > ) (proj2 (zp-iso0 ? )) (proj1 (zp-iso0 ? ))  ) ( zp-iso (subst (λ k → odef k xy) *iso ab )) 
+       fun←  = λ xy ab → getord ( exchg {A} {B} {zπ1 (subst (λ k → odef k xy) *iso ab)} {zπ2 (subst (λ k → odef k xy) *iso ab)}  {_} refl (subst₂ (λ j k → odef j k) *iso (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) ab ))
+     ; fun→  = λ xy ba → getord ( exchg {B} {A} {zπ1 (subst (λ k → odef k xy) *iso ba)} {zπ2 (subst (λ k → odef k xy) *iso ba)}  {_} refl (subst₂ (λ j k → odef j k) *iso (sym (zp-iso (subst (λ k → odef k xy) *iso ba))) ba ))
+     ; funB  = λ xy ab → subst₂ (λ j k → odef j k ) (sym *iso) refl 
+          (exchg (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) (subst (λ k → odef k xy) *iso ab))
+     ; funA  = λ xy ab → subst₂ (λ j k → odef j k ) (sym *iso) refl 
+          (exchg (sym (zp-iso (subst (λ k → odef k xy) *iso ab))) (subst (λ k → odef k xy) *iso ab))
+     ; fiso← = λ xy ab → trans (cong getord ( HE.≅-to-≡ (exchg² refl (ab-pair ? ? ))) ) (trans ? (is-prod (subst (λ k → odef k xy) *iso ab)) )
+     ; fiso→ = λ xy ab → ?
     } where
-        lemma1 : {A B : HOD} {xy : Ordinal} → (ba : odef (* (& (ZFP B A))) xy) → odef (ZFP A B) (
-                & < * (zπ2 (subst (λ k → odef k xy) *iso ba)) , * (zπ1 (subst (λ k → odef k xy) *iso ba)) >  )
-        lemma1 {A} {B} {xy} ba = ? -- with subst (λ k → odef k xy ) *iso ba
-        -- ... | ab-pair ax by = ?
+        getord : {A B : HOD} {xy : Ordinal} → odef (ZFP A B) xy → Ordinal
+        getord {A} {B} {xy} ab = xy
+        is-prod : {A B : HOD} {xy : Ordinal} → (ab : odef (ZFP A B) xy) → getord ab ≡ xy
+        is-prod {A} {B} {xy} ab = refl
+        exchg : {A B : HOD} {x y xy : Ordinal} → xy ≡ & < * x , * y > → odef (ZFP A B) xy → odef (ZFP B A) (& < * y , * x >) 
+        exchg {A} {B} {x} {y} eq (ab-pair {a} {b} ax by ) = subst (λ k → odef (ZFP B A) k) 
+           (cong₂ (λ j k → & < j , k >) (proj2 (prod-≡ lemma2 )) (proj1 (prod-≡ lemma2 )) ) (ab-pair by ax) where
+             lemma2 : < * a , * b > ≡ < * x , * y >
+             lemma2 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq)
+        exchg² : {A B : HOD} {x y xy : Ordinal} → (eq : xy ≡ & < * x , * y >) → (ab : odef (ZFP A B) xy) → exchg refl ( exchg eq ab ) ≅ ab
+        exchg² {A} {B} eq (ab-pair ax by ) = ?
 
 
 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 )