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

diff -r 19f997175d80 -r 02bf7dccc625 src/cardinal.agda
--- a/src/cardinal.agda	Tue Jul 04 18:55:11 2023 +0900
+++ b/src/cardinal.agda	Tue Jul 04 21:49:41 2023 +0900
@@ -42,6 +42,8 @@
 
 open HOD
 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+
 -- record HODBijection (A B : HOD ) : Set n where
 --   field
 --       fun→  : (x : Ordinal ) → odef B  x → Ordinal
@@ -201,8 +203,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 ))  
 
@@ -363,19 +363,31 @@
 
      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 
+    
+     diag3 : {x : Ordinal } → (sx : odef S x) → odef (Power S) (fun← b x sx)
+     diag3 sx = diag2 sx
      
-     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b _ (diag2 sx) ≡ x )
+     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b (fun← b x sx) (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 _ (diag2 sx)) (funB b _ (diag2 sx) )) ) x )  
-        ≡⟨ cong ( λ k →  not (is-S (* k) 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
+        ∎ ) 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 (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) 
 
      diag5 : fun→ b _ (diag2 ss) ≡ s
      diag5 = begin