Is there any meaning to a "nice bijective proof?"

Question

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 specific structures involved, and one feels a bit cheated. [... O]ne still hopes for a really natural, "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.

Answer 1

Baez and Dolan argue that in some cases division is easier than subtraction. In particular, most division problems come from group actions, and Baez and Dolan define a "weak quotient" of a G-set with cardinality precisely the ratio that you want it to be.

Here's what he does. Recall that a groupoid is a category with all morphisms invertible. Two examples: a groupoid with only identity morphisms is naturally a set; a groupoid with only one object is naturally a group; these are two extremes (trivial on the morphism level; trivial on the object level).

I will consider only finite groupoids. Then for each object x, consider the number 1/|Aut(x)|, where Aut(x) = Hom(x,x). This is a class function: if x and y are isomorphic, then |Aut(x)|=|Aut(y)|. Baez and Dolan define the cardinality of a groupoid to be the sum over equivalence classes of 1/|Aut(-)|. The cardinality is preserved under equivalences of groupoids.

Anyway, let X be a set and G a group acting on it. One defines the "action groupoid" to have objects X and morphisms pairs (x,_g_) ∈ X x G, where the source of the morphism is x and the target is gx. Turns out that the cardinality of the action groupoid is |X|/|G|.

(I think that the right way to think about the action groupoid is as some sort of extension, like a semidirect product, of the groupoids X and G, and what's really going on is that you should think of G as a groupoid with 1/|G| many objects.)

Answer 2

Igor Pak wrote a paper in which he defines the notion of an "asymptotically stable" partition bijection, then shows there is no such bijection proving the Rogers-Ramanujan identities.