To what extent can "cardinality" be viewed as a functor? It is common two denote a general forgetful functor $\mathcal{C}\to\mathcal{D}$ as $c\mapsto |c|$, by analogy with the cardinality of a set or the absolute value of a number. To what extent can this be made rigorous?
That is, to what extent can cardinality be viewed as a functor $|\cdot|:\mathsf{Set}\to\mathbb{N}$ from some structure on sets to some structure on natural numbers? What kind of properties does this functor have? I can't think of any possible way to define a "free functor" $F:\mathbb{N}\to\mathsf{Set}$, i.e., there seems to be no canonical "free set" with a given cardinality.
 A: Note: you need to work with either $\mathsf{FinSet}$, the category of (hereditarily small) finite sets, or extend your "category of cardinalities" to $\mathsf{Card}$, the category of (small) cardinalities. Otherwise, the functor $|\,\cdot\,|$ doesn't make sense at all. Let's take the latter option, although it does not matter so much for what follows which one you take.
In ordinary ZFC, cardinalities are in particular all sets. Thus, if we let $\mathsf{Card}$ be the category of cardinalities and functions, then we just have an inclusion functor $i: \mathsf{Card} \to \mathsf{Set}$. In order to give a retraction of this inclusion -- i.e. a cardinality functor $|\,\cdot\,|: \mathsf{Set} \to \mathsf{Card}$, so that $|i(\kappa)| = \kappa$ -- we need something like a global axiom of choice allowing us to associate to each set $A$ a bijection $c_A: A \to |A|$. Then you can define the functor $|\,\cdot\,|$ on morphisms by $|f: A \to B| = c_B \circ f \circ c_A^{-1}$.
Arguably, it makes more sense to say the category $\mathsf{Card}$ should be a posetal category: that is, its objects are still cardinalities, but now there is a morphism $\kappa \to \lambda$ if and only if $\kappa \leq \lambda$. In this case, we can consider the category $\mathsf{Inj}$ of sets with only injections as morphisms. The functor $\mathsf{Card} \to \mathsf{Inj}$ is still basically an inclusion: it takes a morphism $\kappa \leq \lambda$ to the inclusion $\kappa \subseteq \lambda$. In reverse, if there is an injection $A \to B$, then in fact $|A| \leq |B|$, so you send the injection to that 'morphism'.
