# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1688599986 -32400
# Node ID ff69832b5c21d5b9e9d90f8e008d3298f0083196
# Parent  682fe6b32b2aded81d974e5e244eaa1288b0f841
use ==

diff -r 682fe6b32b2a -r ff69832b5c21 src/cardinal.agda
--- 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 = {!!}