Axiom of Choice needed to "categorify" the cardinals? I was playing around in $\mathsf{Set},$ trying to reduce it modulo isomorphisms to make a category $\mathsf{Card},$ letting the objects of $\mathsf{Card}$ be the isomorphism classes of $\mathsf{Set}$ and let the morphisms of $\mathsf{Card}$ be the isomorphism classes of $\mathsf{Set}^\to$ (the arrow category). Unfortunately, I got stuck trying to define composition in the obvious way.
Here's the approach I was taking. Given $a\in\mathsf{Set}$ or $f\in\mathsf{Set}^\to,$ we denote their respective isomorphism classes by $|a|$ and $\bar f.$ I've shown that each $\bar f$ uniquely determines a source and a target $|a|$ and $|b|,$ by taking any $f\in\bar f,$ and letting $a,b$ the source and target of $f$ (this is independent of our choice of $f$). If we have $\bar f:|a|\to|b|$ and $\bar g:|b|\to|c|,$ then there exist $a\in|a|,b\in|b|,c\in|c|,f\in\bar f,$ and $g\in\bar g$ such that $f:a\to b$ and $g:b\to c.$ It seems natural to define $\bar g\bar f:=\overline{gf},$ but I'm having trouble showing independence from the choices of $a,b,c,f,$ and $g.$
I started by taking $f_j:a_j\to b_j$ and $g_j:b_j\to c_j$ for $j=1,2,$ and taking isomorphisms $\langle u_1,v_1\rangle:f_1\to f_2$ and $\langle u_2,v_2\rangle:g_1\to g_2.$ So, $f_2u_1=v_1f_1$ and $g_2u_2=v_2g_1.$ Now, if I could find some iso $u:a_1\to a_2$ such that $\langle u,u_2\rangle:f_1\to f_2,$ then I'd be done. Likewise if I could find an iso $v:c_1\to c_2$ such that $\langle v_1,v\rangle:g_1\to g_2.$ Now, the latter doesn't seem feasible, since there's no guarantee that $v_2$ should map fibers of $g_1$ bijectively to fibers of $g_2.$ I've not had any success demonstrating the former, either.

If I use the Axiom of Choice, then I can show that if $f:A\to B$ and $g:X\to Y$ are isomorphic objects in $\mathsf{Set}^\to$, then for any iso $v:B\to Y,$ there is an iso $u:A\to X$ such that $\langle u,v\rangle:f\to g.$ From there, I can finish the proof that the operation is well (and uniquely) defined. In fact, this result seems to imply the Axiom of Choice, as well, which makes me suspect that it is necessary. If so, would someone be able to outline a proof or provide a reference?
If not, then could someone help me get "unstuck"?

Now, if we stick to isomorphism classes of injective functions, we can categorify the cardinals as a partial order (a well-order iff Choice holds), but I'd like to include more isomorphism classes than that, if possible.

Added: As Eric points out, my difficulties are only to be expected. It would seem, then, that my desires might be fruitless, and that only isomorphism classes of injective functions allow such composition to be well-defined. Am I correct?
 A: 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. 
A: 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.
