# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688461869 -32400
# Node ID 687a4454fae4071e8cb0211032eef7a487b6b5eb
# Parent  1a9859a0b14d0e822a8d94ebe2f73b9ab09767ba
...

diff -r 1a9859a0b14d -r 687a4454fae4 src/cardinal.agda
--- a/src/cardinal.agda	Tue Jul 04 12:06:12 2023 +0900
+++ b/src/cardinal.agda	Tue Jul 04 18:11:09 2023 +0900
@@ -361,26 +361,27 @@
          ca01 : odef (Power S) (fun← b x sx )
          ca01 = funA b x sx
 
-     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 = ?
+     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 
      
-     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b x (diag2 sx) ≡ x )
+     diagn1 : {x : Ordinal } (sx : odef S x ) → ¬ (fun→ b _ (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 (fun→ b _ (diag2 sx)) (funB b _ (diag2 sx) )) ) x )  
         ≡⟨ ? ⟩
           not (is-S (* (fun← b x sx )) x)  
         ≡⟨⟩
           diag  sx 
         ∎ ) where open ≡-Reasoning
 
-     diag5 : fun→ b s (diag2 ss) ≡ s
-     diag5 = ?
+     diag5 : fun→ b _ (diag2 ss) ≡ s
+     diag5 = begin
+        fun→ b _ (diag2 ss) ≡⟨ ? ⟩
+        fun→ b _ (λ _ sx → funA b _ ? _  sx) ≡⟨ ? ⟩
+        s ∎ where open ≡-Reasoning
 
      diag4 : ⊥ 
      diag4 = diagn1 ss diag5