Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1443:19f997175d80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Jul 2023 18:55:11 +0900
parents 687a4454fae4
children 02bf7dccc625
files src/cardinal.agda
diffstat 1 files changed, 3 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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 : ⊥