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

comparison 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
comparison
equal deleted inserted replaced
416:b737a2e0b46e 417:f464e48e18cc
52 onto = {!!} 52 onto = {!!}
53 53
54 record Bijection (A B : Ordinal ) : Set n where 54 record Bijection (A B : Ordinal ) : Set n where
55 field 55 field
56 bfun : Ordinal 56 bfun : Ordinal
57 bfun-isfun : def (Func {!!} {!!} ) bfun 57 bfun-isfun : def (Func (ord→od A) (ord→od B)) bfun
58 bfun-is1-1 : ? 58 bfun-is1-1 : {!!}
59 bfun-isonto : ? 59 bfun-isonto : {!!}
60 60
61 Card : OD 61 Card : OD
62 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x } 62 Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ Bijection a x }