# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1596682235 -32400
# Node ID 47aacf417930c61e1b79ef736d370aaec315aa16
# Parent  f7d66c84bc26bd047f482d73dd526a1c3170c1bf
...

diff -r f7d66c84bc26 -r 47aacf417930 cardinal.agda
--- 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 }