Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1451:682fe6b32b2a
...
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 = {!!}