# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688701228 -32400
# Node ID 43f0c259e6c1a3ccbf589a5330edcab5b5ce7b71
# Parent  c6bc9334a3ee32eaef4020da9f2f041b27ab8091
cantor all done

diff -r c6bc9334a3ee -r 43f0c259e6c1 src/ZProduct.agda
--- a/src/ZProduct.agda	Fri Jul 07 10:43:12 2023 +0900
+++ b/src/ZProduct.agda	Fri Jul 07 12:40:28 2023 +0900
@@ -383,6 +383,16 @@
      ; fiso→ = λ x lt → refl
     }
 
+hodbij-sym : { a b : HOD } → HODBijection a b → HODBijection b a
+hodbij-sym {a} eq = record {
+       fun←  = fun→ eq
+     ; fun→  = fun← eq
+     ; funB  = funA eq
+     ; funA  = funB eq
+     ; fiso← = fiso→  eq
+     ; fiso→ = fiso←  eq
+    } where open HODBijection
+
 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 )))
diff -r c6bc9334a3ee -r 43f0c259e6c1 src/cardinal.agda
--- a/src/cardinal.agda	Fri Jul 07 10:43:12 2023 +0900
+++ b/src/cardinal.agda	Fri Jul 07 12:40:28 2023 +0900
@@ -325,6 +325,15 @@
 ... | case1 a = true
 ... | case2 b = false
 
+fun←eq : {S : HOD} (b : HODBijection (Power S) S ) {x y : Ordinal } → {ax : odef S x} {ax1 : odef S y}  
+    → x ≡ y  → fun← b x ax ≡ fun← b y ax1
+fun←eq {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun← b x k) ( HE.≅-to-≡ ( ∋-irr {S} ax ax1 ))  
+     
+fun→eq : {S : HOD} (b : HODBijection (Power S) S ) {x y : Ordinal } → {ax : odef (Power S) x} {ax1 : odef (Power S) y}  
+    → x ≡ y  → fun→ b x ax ≡ fun→ b y ax1
+fun→eq {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun→ b x k) ( HE.≅-to-≡ ( ∋-irr {Power S} ax ax1 ))  
+     
+
 --    S
 --    t ⊆ S    ( Power S ∋ t )
 --    S   s₀    s₁      ...  sn
@@ -333,7 +342,12 @@
 Cantor1 : { S : HOD } → S c< Power S
 Cantor1 {S} f = diag4 where 
      f1 : Injection (& S) (& (Power S))
-     f1 = record { i→ = λ x sx → & (* x , * x) ; iB = c00 ;  inject = ? }where
+     f1 = record { i→ = λ x sx → & (* x , * x) ; iB = c00 ;  inject = c02 }where
+         c02 : (x y : Ordinal) (ltx : odef (* (& S)) x) (lty : odef (* (& S)) y) →
+            & (* x , * x) ≡ & (* y , * y) → x ≡ y
+         c02 x y ltx lty eq = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (xx=zy→x=y c03 )) where
+             c03 : (* x , * x) =h= (* y , * y)
+             c03 = ord→== eq
          c00 : (x : Ordinal) (lt : odef (* (& S)) x) → odef (* (& (Power S))) (& (* x , * x))
          c00 x lt = subst₂ (λ j k → odef j (& k) ) (sym *iso) refl (λ y z → c01 y (subst (λ k → odef k y ) *iso z  )) where
              c01 : (y : Ordinal ) → odef (* x , * x ) y  → odef S y
@@ -342,7 +356,7 @@
      f2 : Injection (& (Power S)) (& S) 
      f2 = f
      b : HODBijection (Power S) S 
-     b = ? -- subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)   -- this makes check very slow
+     b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)   -- this makes check very slow
 
      -- we have at least one element since Power S contains od∅
      --
@@ -379,8 +393,6 @@
      ... | case2 lt | case1 lt1 | _ = refl
      ... | case2 lt | case2 neg | record { eq = eq1 } = ⊥-elim ( neg ⟪ sn , (λ sx → trans (cong diag ( HE.≅-to-≡ ( ∋-irr {S} sx sn ))) eq1 ) ⟫ )
 
-     fun←eq : {x y : Ordinal } → {ax : odef S x} {ax1 : odef S y}  → x ≡ y  → fun← b x ax ≡ fun← b y ax1
-     fun←eq {x} {x} {ax} {ax1} refl = cong (λ k → fun← b x k) ( HE.≅-to-≡ ( ∋-irr {S} ax ax1 ))  
 
      diagn1 : (n : Ordinal ) → odef S n → ¬ (fun→ b (& Diag) diag3 ≡ n)
      diagn1 n sn dn = ¬t=f (is-S Diag n) (begin
@@ -389,7 +401,7 @@
           not (is-S (* (& Diag)) n)
         ≡⟨ cong (λ k → not (is-S (* k) n)) (sym (fiso← b (& Diag) diag3 )) ⟩
           not (  is-S (* (fun← b (fun→ b (& Diag) diag3) (funB b (& Diag) diag3 ))) n ) 
-        ≡⟨ cong (λ k → not (is-S (* k) n)) ( fun←eq {_} {_} {funB b _ diag3} {sn} dn )   ⟩
+        ≡⟨ cong (λ k → not (is-S (* k) n)) ( fun←eq b {_} {_} {funB b _ diag3} {sn} dn )   ⟩
           not (  is-S (* (fun← b n sn )) n ) 
         ≡⟨ not-isD _ sn  ⟩
           is-S Diag n
@@ -397,11 +409,26 @@
           open ≡-Reasoning
  
      diag4 : ⊥ 
-     diag4 = diagn1  (fun→ b (& Diag) diag3) ? refl
+     diag4 = diagn1  (fun→ b (& Diag) diag3) (funB b (& Diag) diag3) refl
  
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
-Cantor2 = {!!}
+Cantor2 {u} ceq = Cantor1 {u} record { i→ = λ x lt → fun← ceq x (subst (λ k → odef k x) *iso lt) 
+     ; iB = λ x lt → subst₂ (λ j k → odef j k) (sym *iso) refl (funA ceq x (subst (λ k → odef k x) *iso lt))  
+     ; inject = c04 } where
+         c04 :  (x y : Ordinal) (ltx : odef (* (& (Power u))) x) (lty : odef (* (& (Power u))) y) 
+            → fun← ceq x (subst (λ k → odef k x) *iso ltx) ≡ fun← ceq y (subst (λ k → odef k y) *iso lty) → x ≡ y
+         c04 x y ltx lty eq = begin
+           x ≡⟨ sym ( fiso→ ceq x c05 ) ⟩
+           fun→ ceq ( fun← ceq x c05 ) (funA ceq x c05)  ≡⟨ fun←eq (hodbij-sym ceq) eq ⟩
+           fun→ ceq ( fun← ceq y c06 ) (funA ceq y c06)  ≡⟨ fiso→ ceq y c06 ⟩
+           y ∎ where 
+             open ≡-Reasoning
+             c05 : odef (Power u) x
+             c05 = subst (λ k → odef k x) *iso ltx
+             c06 : odef (Power u) y
+             c06 = subst (λ k → odef k y) *iso lty
 
 
 
 
+