# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688694192 -32400
# Node ID c6bc9334a3ee32eaef4020da9f2f041b27ab8091
# Parent  1a9859a0b14d0e822a8d94ebe2f73b9ab09767ba
cantor passed

diff -r 1a9859a0b14d -r c6bc9334a3ee src/OD.agda
--- a/src/OD.agda	Tue Jul 04 12:06:12 2023 +0900
+++ b/src/OD.agda	Fri Jul 07 10:43:12 2023 +0900
@@ -430,7 +430,7 @@
 A ∈ B = B ∋ A
 
 Power : HOD  → HOD
-Power A =  record { od = record { def = λ x → ( ( z : Ordinal) → odef (* x) z → odef A z ) } ; odmax = osuc (& A) 
+Power A =  record { od = record { def = λ x → ( z : Ordinal) → odef (* x) z → odef A z  } ; odmax = osuc (& A) 
        ; <odmax = p00  } where
    p00 :  {y : Ordinal} → ((z : Ordinal) → odef (* y) z → odef A z) → y o< osuc (& A)
    p00 {y} y⊆A = p01 where
@@ -443,6 +443,9 @@
 power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
 power← A t t⊆A z xz = subst (λ k → odef A k ) &iso ( t⊆A  (subst₂ (λ j k → odef j k) *iso (sym &iso) xz ))
 
+Power∋∅ : {S : HOD} → odef (Power S) o∅
+Power∋∅ z xz = ⊥-elim (¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz)  )
+
 Intersection : (X : HOD ) → HOD   -- ∩ X
 Intersection X = record { od = record { def = λ x → (x o≤ & X ) ∧ ( {y : Ordinal} → odef X y → odef (* y) x )} ; odmax = osuc (& X) ; <odmax = λ lt → proj1 lt } 
 
diff -r 1a9859a0b14d -r c6bc9334a3ee src/cardinal.agda
--- a/src/cardinal.agda	Tue Jul 04 12:06:12 2023 +0900
+++ b/src/cardinal.agda	Fri Jul 07 10:43:12 2023 +0900
@@ -6,7 +6,7 @@
 
 open import logic
 -- import OD
-import OD hiding ( _⊆_ )
+import OD 
 
 import ODC
 open import Data.Nat 
@@ -31,9 +31,7 @@
 open OrdUtil O
 open ODUtil O
 
-_⊆_ : ( A B : HOD ) → Set n
-_⊆_ A B = {x : Ordinal } → odef A x → odef B x
-
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
 open _∧_
 open _∨_
@@ -69,7 +67,7 @@
     im00 {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ ( λ j k → j o< k) (trans &iso (sym x=fy)) &iso 
          (c<→o< (subst ( λ k → odef (* b) k) (sym &iso) (iB iab y ay)) )
 
-Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image a iab ⊆ * b 
+Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image a iab ⊆ (* b )
 Image⊆b {a} {b} iab {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k) (sym x=fy) (iB iab y ay)
 
 _=c=_ : ( A B : HOD ) → Set n
@@ -201,8 +199,6 @@
       ... | case1 img = img
       ... | case2 nimg = ⊥-elim ( ncn (a-g ax nimg ) )
 
-      open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-
       fab-eq : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y}  → x ≡ y  → fab x ax ≡ fab y ax1
       fab-eq {x} {x} {ax} {ax1} refl = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 ))  
 
@@ -334,8 +330,8 @@
 --    S   s₀    s₁      ...  sn
 --    t   true  false   ...  false
 ---
-Cantor1 : { S : HOD } → {s : Ordinal } → odef S s → S c< Power S
-Cantor1 {S} {s} ss f = diag4 where 
+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
          c00 : (x : Ordinal) (lt : odef (* (& S)) x) → odef (* (& (Power S))) (& (* x , * x))
@@ -346,45 +342,63 @@
      f2 : Injection (& (Power S)) (& S) 
      f2 = f
      b : HODBijection (Power S) S 
-     b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)
+     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∅
+     --
+
+     p0 : odef (Power S) o∅
+     p0 z xz = ⊥-elim (¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz)  )
+
+     s : Ordinal 
+     s = fun→ b o∅ p0
+
+     ss : odef S s
+     ss = funB b o∅ p0
 
      is-S : (S : HOD) → (x : Ordinal ) →  Bool
      is-S S x with ODC.p∨¬p O (odef S x )
      ... | case1 _ = true
      ... | case2 _ = false
 
-     ---  if t ∋ x then false else true 
-     ---    diag : T → Bool
+     diag : {x : Ordinal} → (sx : odef S x) → Bool 
+     diag {x} sx = is-S (* (fun← b x sx)) x
+
+     Diag : HOD
+     Diag = record { od = record { def = λ x → odef S x ∧ ((sx : odef S x) → diag sx ≡ false) } 
+         ; odmax = & S ; <odmax = odef∧< } 
 
-     diag : {x : Ordinal } → odef S x → Bool
-     diag {x} sx = not (is-S (* (fun← b x sx )) x ) where
-         ca01 : odef (Power S) (fun← b x sx )
-         ca01 = funA b x sx
+     diag3 : odef (Power S) (& Diag)
+     diag3 z xz with subst (λ k → odef k z) *iso xz
+     ... | ⟪ sx , eq ⟫ = sx
+
+     not-isD : (x : Ordinal) → (sn : odef S x)  → not (  is-S (* (fun← b x sn )) x ) ≡ is-S Diag x
+     not-isD x sn with  ODC.p∨¬p O (odef (* (fun← b x sn )) x)  | ODC.p∨¬p O (odef Diag x) | inspect (is-S (* (fun← b x sn ))) x
+     ... | case1 lt | case1 ⟪ sx , eq ⟫ | record { eq = eq1 } = ⊥-elim (¬t=f false (trans (sym eq1) (eq sn )) )
+     ... | case1 lt | case2 lt1 | _ = refl
+     ... | 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 ) ⟫ )
 
-     diag2 : {x : Ordinal } → odef S x → (z : Ordinal) → odef (* x) z → odef S z
-     diag2 {x} sx z xz = funA b x sx z ca02 where
-          ca02 : odef (* (fun← b x sx)) z
-          ca02 = ?
-     
-     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b x (diag2 sx) ≡ x )
-     diagn1 {x} sx dn = ¬t=f (diag sx ) ( begin
-           not (diag  sx  )
-        ≡⟨⟩
-          not ( not (is-S (* (fun← b x sx )) x )) 
-        ≡⟨ ? ⟩
-          not (is-S (* (fun← b (fun→ b x (diag2 sx)) (funB b x (diag2 sx) )) ) x )  
-        ≡⟨ ? ⟩
-          not (is-S (* (fun← b x sx )) x)  
-        ≡⟨⟩
-          diag  sx 
-        ∎ ) where open ≡-Reasoning
+     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 ))  
 
-     diag5 : fun→ b s (diag2 ss) ≡ s
-     diag5 = ?
-
+     diagn1 : (n : Ordinal ) → odef S n → ¬ (fun→ b (& Diag) diag3 ≡ n)
+     diagn1 n sn dn = ¬t=f (is-S Diag n) (begin
+          not (is-S Diag n)
+        ≡⟨ cong (λ k → not (is-S k n)) (sym *iso) ⟩
+          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 )   ⟩
+          not (  is-S (* (fun← b n sn )) n ) 
+        ≡⟨ not-isD _ sn  ⟩
+          is-S Diag n
+        ∎ ) where 
+          open ≡-Reasoning
+ 
      diag4 : ⊥ 
-     diag4 = diagn1 ss diag5
-
+     diag4 = diagn1  (fun→ b (& Diag) diag3) ? refl
+ 
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
 Cantor2 = {!!}