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

changeset 1452:ff69832b5c21

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use ==
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Jul 2023 08:33:06 +0900
parents 682fe6b32b2a
children
files src/cardinal.agda
diffstat 1 files changed, 3 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Thu Jul 06 00:31:25 2023 +0900
+++ b/src/cardinal.agda	Thu Jul 06 08:33:06 2023 +0900
@@ -389,6 +389,9 @@
      diag5 : fun← b (fun→ b (& (DIAG ss)) (Pdiag ss)) (funB b (& (DIAG ss)) (Pdiag ss)) ≡ & (DIAG ss)
      diag5 = fiso← b  (& (DIAG ss)) (Pdiag ss)
 
+     diag6 : ¬ (* (fun← b (fun→ b (& (DIAG ss)) (Pdiag ss)) (funB b (& (DIAG ss)) (Pdiag ss))) =h= DIAG ss)
+     diag6 = ?
+
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
 Cantor2 = {!!}