--- a/src/cardinal.agda	Tue Jul 04 10:14:27 2023 +0900
+++ b/src/cardinal.agda	Tue Jul 04 12:06:12 2023 +0900
@@ -335,7 +335,7 @@
 --    t   true  false   ...  false
 ---
 Cantor1 : { S : HOD } → {s : Ordinal } → odef S s → S c< Power S
-Cantor1 {S} {s} ss f = diagn1 ss ? where
+Cantor1 {S} {s} ss 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))
@@ -357,19 +357,33 @@
      ---    diag : T → Bool
 
      diag : {x : Ordinal } → odef S x → Bool
-     diag {x} sx = not (is-S (* (fun← b x ? )) x )  where
-         ca00 :  odef (Power S) x
-         ca01 : odef (Power S) (fun← b x ? )
-         ca01 = ? -- funA b x ?
-         ca00 z xz = ? 
+     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
 
-     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b x ? ≡ x )
+     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 )) 
         ≡⟨ ? ⟩
-           diag  sx 
+          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
 
+     diag5 : fun→ b s (diag2 ss) ≡ s
+     diag5 = ?
+
+     diag4 : ⊥ 
+     diag4 = diagn1 ss diag5
 
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
 Cantor2 = {!!}