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

changeset 1451:682fe6b32b2a

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 Thu, 06 Jul 2023 00:31:25 +0900
parents b7f6eb9eaf0d
children ff69832b5c21
files src/cardinal.agda
diffstat 1 files changed, 8 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/src/cardinal.agda	Wed Jul 05 12:35:36 2023 +0900
+++ b/src/cardinal.agda	Thu Jul 06 00:31:25 2023 +0900
@@ -335,7 +335,7 @@
 --    t   true  false   ...  false
 ---
 Cantor1 : { S : HOD } → S c< Power S
-Cantor1 {S}  f = diag4 where 
+Cantor1 {S}  f = ? where 
      f1 : Injection (& S) (& (Power S))
      f1 = record { i→ = λ x sx → & (* x , * x) ; iB = c00 ;  inject = ? }where
          c00 : (x : Ordinal) (lt : odef (* (& S)) x) → odef (* (& (Power S))) (& (* x , * x))
@@ -380,11 +380,14 @@
      ss : odef S s
      ss = funB b o∅ p0
 
+     --  DIAG is not in domain of fun→ b, but not in codomain of (fun← b ? ? )
+     -- 
 
-     diag4 : ⊥ 
-     diag4 with ODC.p∨¬p O ( odef (* (fun← b s ss)) s)
-     ... | case1 y  = ?
-     ... | case2 n  = ?
+     diag4 : odef S (fun→ b (& (DIAG ss)) (Pdiag ss))
+     diag4 = funB b (& (DIAG ss)) (Pdiag ss)
+
+     diag5 : fun← b (fun→ b (& (DIAG ss)) (Pdiag ss)) (funB b (& (DIAG ss)) (Pdiag ss)) ≡ & (DIAG ss)
+     diag5 = fiso← b  (& (DIAG ss)) (Pdiag ss)
 
 Cantor2 : { u : HOD } → ¬ ( u =c=  Power u )
 Cantor2 = {!!}