From Zeilberger's PCM article on enumerative combinatorics:

The reaction of the combinatorial enumeration community to the involution principle was mixed. On the one hand it had the universal appeal of a general principle... On the other hand, its universality is also a major drawback, since involution-principle proofs usually do not give any insight into the

specificstructures involved, and one feels a bit cheated. [... O]ne still hopes for areallynatural, "involution-principle-free proof."

The quest for bijective proofs really is, at heart, the quest to categorify an equation proved via "decategorified" arithmetic, to provide an explicit family of isomorphisms in the category of finite sets (or the category of finite sets and bijections, I don't think it matters). So categorifying multiplication and addition is easy -- they just correspond to product and coproduct of sets, respectively. Categorifying subtraction is trickier, but that's what the involution principle does for us. (On a tangential note, I know that categorifying division is [in]famously hard in the category of sets -- is it anything like as hard when we talk about finite sets? ETA: Looking at Conway's paper, the answer seems to be "yes and no." No, because with finite sets it's kosher to use a bijection between a set of size n and {0, 1, ..., n-1}; yes, because this is sort of like a "finitary Axiom of Choice," and in particular it's not canonical.)

So is there any real meaning, in a categorical sense, to the enumerative-combinatorial dream of "really nice proofs?" Or will there necessarily be identities that can only be proved bijectively by categorifying, in a general and universal way, their "manipulatorics" proofs?

Edit: So philosophically this is a category-theory question, and it'd be nice to have it as a "real" category-theory question. Here's my (*very* rough) attempt at phrasing it as such.

Let T be a topos where we can categorify addition, multiplication, and subtraction of natural numbers. Then, are there functors between T and FinSet that preserve these decategorifications? If so, then I think maybe we can ask the question in terms of topos theory, although maybe not -- I don't really know much topos theory, so I'm certainly having trouble.