--- a/src/cardinal.agda	Wed Jul 05 07:39:17 2023 +0900
+++ b/src/cardinal.agda	Wed Jul 05 10:57:43 2023 +0900
@@ -334,8 +334,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))
@@ -348,82 +348,42 @@
      b : HODBijection (Power S) S 
      b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1)
 
-     is-S : (S : HOD) → (x : Ordinal ) →  Bool
-     is-S S x with ODC.p∨¬p O (odef S x )
-     ... | case1 _ = true
-     ... | case2 _ = false
-
      diag2 : {x : Ordinal } → (sx : odef S x) → (z : Ordinal) → odef (* (fun← b x sx)) z → odef S z
      diag2 {x} sx z xz = funA b x sx z xz 
     
-     ---  if t ∋ x then false else true 
-     ---    diag : T → Bool
-
-     is-PowerS : {x : Ordinal } → (sx : odef S x) → is-S (* (fun← b x sx )) x  ≡ true
-     is-PowerS {x} sx with ODC.p∨¬p O (odef (* (fun← b x sx )) x ) 
-     ... | case1 _ = refl
-     ... | case2 nsx = ⊥-elim (nsx d00 ) where
-            d01 : x ≡ fun→ b x (ca02 sx)
-            d01 = ?
-            d00 : odef (* (fun← b x sx )) x  
-            d00 = ?
-
-     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
-
-     record Diag (x : Ordinal) : Set n where
-        field
-           sx : odef S x
-           is-diag : is-S (* (fun← b x sx )) x  ≡ false
-
-     diag0 : HOD
-     diag0 = record { od = record { def = λ x → Diag x } ; odmax = & S ; <odmax = ? }
-
-     PSD : odef (Power S) (& diag0)
-     PSD z xz = Diag.sx ( subst (λ k → odef k z) *iso xz)
-
      diag3 : {x : Ordinal } → (sx : odef S x) → odef (Power S) (fun← b x sx)
      diag3 sx = diag2 sx
 
-     f→diagn=n : {x : Ordinal } → odef (Power S) x → Set n
-     f→diagn=n {x} psx = fun→ b x psx ≡ x
-     
-     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b (& diag0) PSD ≡ x )
-     diagn1 {x} sx dn = ¬t=f (diag sx ) ( begin
-           not (diag  sx  )
-        ≡⟨⟩
-          not ( not (is-S (* (fun← b x sx )) x )) 
-        ≡⟨ cong not diag00 ⟩
-          not (is-S (* (fun← b (fun→ b (fun← b x sx) (diag2 sx)) (funB b (fun← b x sx) (diag2 sx) )) ) x )  
-        ≡⟨ cong ( λ k →  not (is-S (* k) x)) diag01  ⟩
-          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 ))  
-          diag00 : not (is-S (* (fun← b x sx )) x ) ≡ is-S (* (fun← b (fun→ b _ (diag2 sx)) (funB b _ (diag2 sx) )) ) x 
-          diag00 = begin
-            not (is-S (* (fun← b x sx )) x ) ≡⟨ ? ⟩
-            is-S (* (fun← b x sx) )  x  ≡⟨ cong (λ k → is-S (* k) x) (sym (fiso← b (fun← b x sx) (diag2 sx) )) ⟩
-            is-S (* (fun← b (fun→ b (fun← b x sx) (diag2 sx)) (funB b (fun← b x sx) (diag2 sx) )) ) x  ∎
-          diag01 : fun← b (fun→ b (fun← b x sx) (diag2 sx)) (funB b (fun← b x sx) (diag2 sx) ) ≡ fun← b x sx 
-          diag01 = fun←eq (fiso→ b x sx) 
+     diag : {x : Ordinal } → (sx : odef S x) → (z : Ordinal) → Set n
+     diag {x} sx z with trio< x z | ODC.p∨¬p O ( odef (* (fun← b x sx)) x)
+     ... | tri< a ¬b ¬c | n = odef  (* (fun← b x sx)) z 
+     ... | tri> ¬a ¬b c | n = odef  (* (fun← b x sx)) z 
+     ... | tri≈ ¬a b₁ ¬c | case1 y = ¬ odef S z
+     ... | tri≈ ¬a b₁ ¬c | case2 n = odef S z
+
+     DIAG : {x : Ordinal } → (sx : odef S x) → HOD
+     DIAG {x} sx = record { od = record { def = λ z → diag sx z  } ; odmax = ? ; <odmax = ? } 
 
-     diag6 : fun→ b (& diag0) PSD ≡ s
-     diag6 = ?
+     Pdiag : {x : Ordinal} → (sx : odef S x) → odef (Power S) (& (DIAG sx))
+     Pdiag {x} sx z xz with trio< x z | ODC.p∨¬p O ( odef (* (fun← b x sx)) x) | subst (λ k → odef k z) *iso xz
+     ... | tri< a ¬b ¬c | n | u = funA b x sx z u
+     ... | tri> ¬a ¬b c | n | u = funA b x sx z u
+     ... | tri≈ ¬a refl ¬c | case1 x₁ | u = ⊥-elim ( u sx )
+     ... | tri≈ ¬a refl ¬c | case2 x₁ | u = u
 
-     diag5 : fun→ b _ (diag2 ss) ≡ s
-     diag5 = begin
-        fun→ b _ (diag2 ss) ≡⟨ refl ⟩
-        fun→ b _ (λ _ sx → funA b _ ss _  sx) ≡⟨ fiso→ b s ss ⟩
-        s ∎ where open ≡-Reasoning
+     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
 
      diag4 : ⊥ 
-     diag4 = diagn1 ? ? 
+     diag4 with ODC.p∨¬p O ( odef (* (fun← b s ss)) s)
+     ... | case1 y  = ?
+     ... | case2 n  = ?
 
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
 Cantor2 = {!!}