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

diff cardinal.agda @ 417:f464e48e18cc

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 Fri, 31 Jul 2020 11:21:27 +0900
parents b737a2e0b46e
children 53422a8ea836
line wrap: on
line diff
--- a/cardinal.agda	Thu Jul 30 21:45:49 2020 +0900
+++ b/cardinal.agda	Fri Jul 31 11:21:27 2020 +0900
@@ -54,9 +54,9 @@
 record Bijection (A B : Ordinal ) : Set n where
    field
        bfun : Ordinal
-       bfun-isfun : def (Func {!!} {!!} )  bfun
-       bfun-is1-1 : ?
-       bfun-isonto : ?
+       bfun-isfun : def (Func (ord→od A) (ord→od B))  bfun
+       bfun-is1-1 : {!!}
+       bfun-isonto : {!!}
        
 Card : OD
 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }