# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688510357 -32400
# Node ID 0fc58fc7fd17b22bfc57fb2323419165cbbeaca9
# Parent  02bf7dccc6257cadbfd70524cf9c1b86826c6417
...

diff -r 02bf7dccc625 -r 0fc58fc7fd17 src/cardinal.agda
--- a/src/cardinal.agda	Tue Jul 04 21:49:41 2023 +0900
+++ b/src/cardinal.agda	Wed Jul 05 07:39:17 2023 +0900
@@ -353,21 +353,44 @@
      ... | 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
 
-     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 
-    
+     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 (fun← b x sx) (diag2 sx) ≡ 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  )
         ≡⟨⟩
@@ -385,10 +408,14 @@
           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) 
 
+     diag6 : fun→ b (& diag0) PSD ≡ s
+     diag6 = ?
+
      diag5 : fun→ b _ (diag2 ss) ≡ s
      diag5 = begin
         fun→ b _ (diag2 ss) ≡⟨ refl ⟩
@@ -396,7 +423,7 @@
         s ∎ where open ≡-Reasoning
 
      diag4 : ⊥ 
-     diag4 = diagn1 ss diag5
+     diag4 = diagn1 ? ? 
 
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
 Cantor2 = {!!}