Here
Card is the
category whose
objects are
cardinal numbers and whose
morphisms f:κ→λ are just
functions (which
act as
witness to κ≤λ). The
category Ordinals is
defined likewise over the collection of all
ordinal numbers. And
WellOrd is the
order category of
well-orderings.