Axiom of Choice needed to "categorify" the cardinals?

The construction you're looking for is called taking a skeleton of a category. In general, doing this requires picking a representative of each isomorphism class of object, and this requires even more than the axiom of choice for a large category like $\text{Set}$: it requires the axiom of global choice. (In particular there is no way of producing skeletons by simply quotienting the set of objects by isomorphism, because as Eric Wofsey points out in the comments, there's no way to make this compatible with composition of morphisms.)

But in some sense all of this is against the spirit of categorification. You should regard $\text{Set}$ itself as already being a natural categorification of the cardinals.


As I commented, composition is not well-defined on isomorphism classes in $\mathsf{Set}^\to$, and this has nothing to do with Choice. In fact, if you want isomorphic maps in $\mathsf{Set}^\to$ to be equal and also for composition to be well-defined, then any two maps $X\to Y$ must be equal for any cardinalities $X$ and $Y$! To see this, take any two maps $f_0,f_1:X\to Y$ and consider $g:X\to X\times\{0,1\}$ given by $i(x)=(x,0)$ and $g:X\times\{0,1\}\to Y$ given by $g(x,0)=f_0(x)$ and $g(x,1)=f_1(x)$. Then $gi=f_0$. But if $h:X\times \{0,1\}\to X\times\{0,1\}$ swaps the second coordinates, then $ghi=f_1$, and $h\cong 1$ in $\mathsf{Set}^\to$. We thus conclude that $f_0$ and $f_1$ must be equal. (This argument works with $\mathsf{Set}$ replaced by any category with binary coproducts.)

As you mention, you can avoid this problem by restricting to injective maps. Then it is easy to see that composition is well-defined, and this does not use the axiom of choice. Note, however, that this gives something more interesting than a poset: if $\kappa$ and $\lambda$ are cardinals, then maps $\kappa\to\lambda$ are in bijection with cardinals $\mu$ such that $\kappa+\mu=\lambda$ (namely, $\mu$ is the cardinality of the complement of the image of the injection). Composition of maps then corresponds to adding the $\mu$s.

Alternatively, as Qiaochu says, you can just not ask for isomorphic maps to be equal and define maps by just choosing a representative set of each cardinality, giving a skeleton of $\mathsf{Set}$. Without Choice, it is consistent that it is impossible to do this, according to this answer (see this paper for a proof). Note that in fact if you can define any category isomorphic to a skeleton of $\mathsf{Set}$ (regardless of how exactly you construct it), then you obtain a choice of a representative of each cardinality, by considering the Hom-sets $\operatorname{Hom}(1,X)$ in your category.