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

diff -r 687a4454fae4 -r 19f997175d80 src/cardinal.agda
--- a/src/cardinal.agda	Tue Jul 04 18:11:09 2023 +0900
+++ b/src/cardinal.agda	Tue Jul 04 18:55:11 2023 +0900
@@ -371,7 +371,7 @@
           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)) ?  ⟩
           not (is-S (* (fun← b x sx )) x)  
         ≡⟨⟩
           diag  sx 
@@ -379,8 +379,8 @@
 
      diag5 : fun→ b _ (diag2 ss) ≡ s
      diag5 = begin
-        fun→ b _ (diag2 ss) ≡⟨ ? ⟩
-        fun→ b _ (λ _ sx → funA b _ ? _  sx) ≡⟨ ? ⟩
+        fun→ b _ (diag2 ss) ≡⟨ refl ⟩
+        fun→ b _ (λ _ sx → funA b _ ss _  sx) ≡⟨ fiso→ b s ss ⟩
         s ∎ where open ≡-Reasoning
 
      diag4 : ⊥