# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1685663533 -32400
# Node ID 968feed7cf645e6a1a9a268eb350c190425a2f78
# Parent  37f28f4276611d9263802355d91b60b70b081506
ZPmirror

diff -r 37f28f427661 -r 968feed7cf64 src/OD.agda
--- a/src/OD.agda	Thu Jun 01 22:15:17 2023 +0900
+++ b/src/OD.agda	Fri Jun 02 08:52:13 2023 +0900
@@ -397,25 +397,30 @@
       → RXCod (* (& X)) C (λ y xy → ψ y (subst (λ k → k ∋ y) *iso xy))
 cod-conv X ψ {C} rc = record { ≤COD = λ {x} lt → RXCod.≤COD rc (subst (λ k → odef k (& x)) *iso lt) }
 
-Replace'-iso : (X : HOD) → (ψ : (x : HOD) → X ∋ x → HOD) → {C : HOD} → (rc : RXCod X C ψ   )
+Replace'-iso : {X Y : HOD} → {fx : (x : HOD) → X ∋ x → HOD} {fy : (x : HOD) → Y ∋ x → HOD}
+    → {CX : HOD} → (rcx : RXCod X CX fx  ) → {CY : HOD} → (rcy : RXCod Y CY fy   )
+      → X ≡ Y →  ( (x :  HOD) → (xx : X ∋ x ) → (yy : Y ∋ x ) → fx _ xx ≡ fy _ yy )
+      → Replace' X fx rcx ≡ Replace' Y fy rcy
+Replace'-iso {X} {X} {fx} {fy} _ _ refl eq  = ==→o≡ record { eq→ = ri0 ; eq← = ri1 } where
+     ri0 : {x : Ordinal} → Replaced1 X (λ z xz → & (fx (* z) (subst (odef X) (sym &iso) xz))) x 
+                         → Replaced1 X (λ z xz → & (fy (* z) (subst (odef X) (sym &iso) xz))) x
+     ri0 {x} record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = az ; x=ψz = trans x=ψz (cong (&) ( eq _ xz xz ))  } where
+         xz : X ∋ * z
+         xz = subst (λ k → odef X k ) (sym &iso) az
+     ri1 : {x : Ordinal} → Replaced1 X (λ z xz → & (fy (* z) (subst (odef X) (sym &iso) xz))) x 
+                         → Replaced1 X (λ z xz → & (fx (* z) (subst (odef X) (sym &iso) xz))) x
+     ri1 {x} record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = az ; x=ψz = trans x=ψz (cong (&) (sym ( eq _ xz xz )))  } where
+         xz : X ∋ * z
+         xz = subst (λ k → odef X k ) (sym &iso) az
+
+Replace'-iso1 : (X : HOD) → (ψ : (x : HOD) → X ∋ x → HOD) → {C : HOD} → (rc : RXCod X C ψ   )
       → Replace' (* (& X)) (λ y xy → ψ y (subst (λ k → k ∋ y ) *iso xy) ) (cod-conv X ψ rc)
          ≡ Replace' X ( λ y xy → ψ y xy ) rc 
-Replace'-iso X ψ rc = ==→o≡ record { eq→ = ri0 ; eq← = ri1 } where
-    ri2 : {z : Ordinal } (a b : X ∋ (* z)) → & (ψ (* z) a) ≡ & (ψ (* z) b)
-    ri2 {z} a b = cong (λ k → & (ψ (* z) k)) ( HE.≅-to-≡ ( ∋-irr {X} {& (* z)} a b ) )
-    ri0 : {x : Ordinal} 
-        → Replaced1 (* (& X)) (λ z xz → & (ψ (* z) (subst (λ k → k ∋ * z) *iso (subst (odef (* (& X))) (sym &iso) xz)))) x 
-        → Replaced1 X (λ z xz → & (ψ (* z) (subst (odef X) (sym &iso) xz))) x
-    ri0 {x} record { z = z ; az = az ; x=ψz = refl } = record { z = z ; az = subst (λ k → odef k z) *iso az 
-       ; x=ψz = ri2 (subst (λ k → k ∋ * z) *iso (subst (odef (* (& X))) (sym &iso) az))  
-                    (subst (odef X) (sym &iso) (subst (λ k → odef k z) *iso az) ) }  
-    ri1 : {x : Ordinal} 
-        → Replaced1 X (λ z xz → & (ψ (* z) (subst (odef X) (sym &iso) xz))) x
-        → Replaced1 (* (& X)) (λ z xz → & (ψ (* z) (subst (λ k → k ∋ * z) *iso (subst (odef (* (& X))) (sym &iso) xz)))) x 
-    ri1 {x} record { z = z ; az = az ; x=ψz = refl } = record { z = z ; az = subst (λ k → odef k z) (sym *iso) az 
-       ; x=ψz = ri2 (subst (λ k → odef X k) (sym &iso) az  )   -- brain damaged below
-           (subst (λ k → k ∋ * z) *iso (subst (odef (* (& X))) (sym &iso) (subst (λ k → odef k z) (sym *iso) az))) } 
-
+Replace'-iso1 X ψ rc = Replace'-iso {* (& X)} {X} {λ y xy → ψ y (subst (λ k → k ∋ y ) *iso xy) } { λ y xy → ψ y xy } 
+    (cod-conv X ψ rc) rc 
+    *iso (λ x xx yx → fi00 x xx yx ) where
+      fi00 : (x : HOD ) → (xx : (* (& X)) ∋ x ) → (yx : X ∋ x) →  ψ x (subst (λ k → k ∋ x) *iso xx) ≡ ψ x yx
+      fi00 x xx yx = cong (λ k → ψ x k ) ( HE.≅-to-≡ ( ∋-irr {X} {& x} (subst (λ k → k ∋ x) *iso xx) yx ) )
 
 -- replacement←1 : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace1 X ψ ∋ ψ x
 -- replacement←1 {ψ} X x lt = record { z = & x ; az = lt  ; x=ψz = cong (λ k → & (ψ k)) (sym *iso) }
diff -r 37f28f427661 -r 968feed7cf64 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Thu Jun 01 22:15:17 2023 +0900
+++ b/src/Tychonoff.agda	Fri Jun 02 08:52:13 2023 +0900
@@ -471,7 +471,7 @@
                   cong (λ k → Replace' (* (& (ZFP q Q))) k ? ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy})))) 
                       ⟩
                   Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)  ))) ?
-                     ≡⟨ Replace'-iso _  ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ? ⟩
+                     ≡⟨ Replace'-iso _  ? ? ?  ⟩
                   Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ?  ≡⟨ refl ⟩
                   fx→px fq ≡⟨ fx→px1 aq fq  ⟩
                   q ∎ where open ≡-Reasoning
@@ -649,11 +649,7 @@
               ty10 : Replace' (* (& (ZFP P q ))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ?  ≡ q
               ty10 = begin
                   Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ?
-                     ≡⟨
-                  cong (λ k → Replace' (* (& (ZFP P q ))) k ? ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy}))))
-                      ⟩
-                  Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)  ))) ?
-                     ≡⟨ Replace'-iso _  ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ? ⟩
+                     ≡⟨ Replace'-iso _  ? ? ?  ⟩
                   Replace' (ZFP P q ) ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ?  ≡⟨ refl ⟩
                   fx→qx fq ≡⟨ fx→qx1 ap fq  ⟩
                   q ∎ where open ≡-Reasoning
diff -r 37f28f427661 -r 968feed7cf64 src/ZProduct.agda
--- a/src/ZProduct.agda	Thu Jun 01 22:15:17 2023 +0900
+++ b/src/ZProduct.agda	Fri Jun 02 08:52:13 2023 +0900
@@ -242,9 +242,6 @@
             * x ≡⟨ sym (cong (*) (ty32 pp qx  )) ⟩
             * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx  ))) ∎ where open ≡-Reasoning
 
-⊆-ZFP : {A B : HOD} {X Y x y : HOD} → X ⊆ A → Y ⊆ B → ZFP X Y ⊆ ZFP A B
-⊆-ZFP {A} {B} {X} {y} X<A Y<B (ab-pair xx yy) = ab-pair (X<A xx) (Y<B yy)
-
 record Func (A B : HOD) : Set n where
     field
        func : {x : Ordinal } → odef A x → Ordinal
@@ -357,6 +354,38 @@
 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 : HOD} {X Y x y : HOD} → X ⊆ A → Y ⊆ B → ZFP X Y ⊆ ZFP A B
+⊆-ZFP {A} {B} {X} {y} X<A Y<B (ab-pair xx yy) = ab-pair (X<A xx) (Y<B yy)
+
+record ZPC (A B C : HOD) ( cab : C ⊆ ZFP A B ) (x : Ordinal) : Set n where
+    field
+       a b : Ordinal
+       aa : odef A a
+       bb : odef B b
+       c∋ab : odef C (& < * a , * b > )
+       x=ba : x ≡ & < * b , * a >
+
+ZPmirror : (A B C : HOD) → C  ⊆ ZFP A B → HOD
+ZPmirror A B C cab = record { od = record { def = λ x → ZPC A B C cab x } ; odmax = osuc (& (Power (Union (B , A)))) ; <odmax = lemma0 } where
+        lemma0 : {x : Ordinal } →  ZPC A B C cab x → x o< osuc (& ( Power ( Union (B , A )) ))
+        lemma0 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = subst (λ k → k o< _) (sym x=ba) lemma1  where
+            lemma1 : & < * b , * a > o< osuc (& (Power (Union (B , A))))
+            lemma1 = ⊆→o≤ (ZFP<AB (subst (λ k → odef B k) (sym &iso) bb) (subst (λ k → odef A k) (sym &iso) aa)  )
+
+ZPmirror-iso : (A B C : HOD)  → (cab : C  ⊆ ZFP A B ) → ( {x y : HOD} → C ∋ < x , y > →  ZPmirror A B C cab ∋ < y , x > ) 
+                                                       ∧ ( {x y : HOD} →  ZPmirror A B C cab ∋ < y , x > → C ∋ < x , y > )
+ZPmirror-iso A B C cab = ⟪ zs00 refl   , zs01 ⟫ where
+    zs00 : {x y : HOD} → {z : Ordinal} → z ≡ & < x , y > → odef C z → ZPmirror A B C cab ∋ < y , x >
+    zs00 {x} {y} {z} eq cz with cab cz
+    ... | ab-pair {a} {b} aa bb = record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = cz 
+       ; x=ba = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso  *iso  (cong (*) eq)))))  
+                                            (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso  *iso  (cong (*) eq))))) }
+    zs01 : {x y : HOD} → ZPmirror A B C cab ∋ < y , x > → C ∋ < x , y >
+    zs01 {x} {y} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = subst (λ k → odef C k ) zs02 c∋ab where
+        zs02 : & < * a , * b > ≡ & < x , y >
+        zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso  *iso  (cong (*) x=ba)))))  
+                                           (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso  *iso  (cong (*) x=ba))))) 
+
 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
    zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x