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

changeset 426:47aacf417930

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 Aug 2020 11:50:35 +0900
parents f7d66c84bc26
children 9b0630f03c4b
files cardinal.agda
diffstat 1 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/cardinal.agda	Wed Aug 05 19:37:07 2020 +0900
+++ b/cardinal.agda	Thu Aug 06 11:50:35 2020 +0900
@@ -70,9 +70,9 @@
 
 record Injection (A B : Ordinal ) : Set n where
    field
-       i→  : (x : Ordinal ) → odef (* B)  x → Ordinal
-       iA  : (x : Ordinal ) → ( lt : odef (* B)  x ) → odef (* A) ( i→ x lt )
-       iiso : (x y : Ordinal ) → ( ltx : odef (* B)  x ) ( lty : odef (* B)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y  
+       i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
+       iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x lt )
+       iiso : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y  
 
 record Bijection (A B : Ordinal ) : Set n where
    field
@@ -90,7 +90,7 @@
 A =c= B = Bijection ( & A ) ( & B )
 
 _c<_ : ( A B : HOD ) → Set n
-A c< B = Injection (& A)  (& B)
+A c< B = ¬ ( Injection (& A)  (& B) )
 
 Card : OD
 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }