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

diff -r e7743ac5a070 -r c077532416d9 src/ZProduct.agda
--- a/src/ZProduct.agda	Wed Apr 05 08:09:49 2023 +0900
+++ b/src/ZProduct.agda	Wed Apr 05 09:00:53 2023 +0900
@@ -162,11 +162,11 @@
        zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
        ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba) 
 
-ZFPproj1 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
-ZFPproj1 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ1 (X⊆P px) )) 
+ZPI1 : (A B : HOD) → HOD
+ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px )) 
 
-ZFPproj2 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
-ZFPproj2 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ2 (X⊆P px) )) 
+ZPI2 : (A B  : HOD) → HOD
+ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 px )) 
 
 ZFProj1-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
 ZFProj1-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
@@ -212,17 +212,17 @@
        iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x lt )
        iiso : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y
 
-record OrdBijection (A B : Ordinal ) : Set n where
+record HODBijection (A B : HOD ) : Set n where
    field
-       fun←  : (x : Ordinal ) → odef (* A)  x → Ordinal
-       fun→  : (x : Ordinal ) → odef (* B)  x → Ordinal
-       funB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( fun← x lt )
-       funA  : (x : Ordinal ) → ( lt : odef (* B)  x ) → odef (* A) ( fun→ x lt )
-       fiso← : (x : Ordinal ) → ( lt : odef (* B)  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
-       fiso→ : (x : Ordinal ) → ( lt : odef (* A)  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
+       fun←  : (x : Ordinal ) → odef A  x → Ordinal
+       fun→  : (x : Ordinal ) → odef B  x → Ordinal
+       funB  : (x : Ordinal ) → ( lt : odef A  x ) → odef B ( fun← x lt )
+       funA  : (x : Ordinal ) → ( lt : odef B  x ) → odef A ( fun→ x lt )
+       fiso← : (x : Ordinal ) → ( lt : odef B  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
+       fiso→ : (x : Ordinal ) → ( lt : odef A  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
 
-ordbij-refl : { a b : Ordinal } → a ≡ b → OrdBijection a b
-ordbij-refl {a} refl = record {
+hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b
+hodbij-refl {a} refl = record {
        fun←  = λ x _ → x 
      ; fun→  = λ x _ → x 
      ; funB  = λ x lt → lt
@@ -231,28 +231,21 @@
      ; fiso→ = λ x lt → refl
     }
 
-ZFPsym : (A B  : HOD) → OrdBijection (& (ZFP A B)) (& (ZFP B A))
+ZFPsym : (A B  : HOD) → HODBijection (ZFP A B) (ZFP (ZPI2 A B) (ZPI1 A B))
 ZFPsym A B = record {
-       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)) )
+       fun←  = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) >
+     ; fun→  = λ xy ab → & < * ( zπ2 ab) , * ( zπ1 ab) >
+     ; funB  = pj2
+     ; funA  = ?
+     ; fiso← = λ xy ab → ?
      ; fiso→ = λ xy ab → ?
     } where
-        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 ) = ?
+       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 ? ?
 
 
 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 )