### changeset 426:47aacf417930

...
author Shinji KONO Thu, 06 Aug 2020 11:50:35 +0900 f7d66c84bc26 9b0630f03c4b cardinal.agda 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 }```