Say

**C**is a

*graded category*if it's a category and every object in

**C**has a natural number associated with it, naming which "grade" it belongs to. There are no particular requirements of arrows; there may well be arrows stretching from one grade to another. Say a

*graded functor*is a functor that preserves grades of objects.

__FinOrd__is a very boring example of a graded category: for every natural number n, it has one object, call it n, at grade n, and it has one arrow from n to n' for each strict monotone mapping of the ordinal n into n'. If

**C**is a graded category, let the category of

*(call it Bal*

**C**-ballots_{C}) be

**C**

^{FinOrdop}, the category of graded functors from

__FinOrd__

^{op}to

**C**, with arrows being natural transformations between these functors. We say

**C**has finite products as a graded category if each subcategory of

**C**obtained by restricting to one grade does. Conjecture that's almost certainly true: If

**C**has finite products as a graded category, then Bal

_{C}does, and they are computed pointwise. A

*social choice function*for B (for a population of m voters) is a left inverse to the diagonal natural transformation Δ : B → B

^{m}:

__FinOrd__

^{op}→

**C**, i.e. a natural transformation sc: B

^{m}→ B such that sc ° Δ = id.

What's beautiful is that the naturality condition encodes IIR, and the left inverse condition encodes unanimity. I'm getting mixed signals from the internet about whether whether Arrow's theorem actually requires monotonicity or not (I was pretty sure it did) but if it didn't, I can stop right here and say for B being specifically the

__Sets__-ballot that takes n to the set of strict linear orders on n, (with the action on arrows being the evident restriction maps) the only social choice functions are projections, i.e. dictatorships. If you need to express monotonicity, then instead of

__Sets__take the graded category

__Pref__, in which an object at grade n is a set with n different poset structures on it ≤

_{1}, ..., ≤

_{n}, and an arrow from C at grade n to D at grade m is a strict monotone map f : m → n and a map g : C → D such that c ≤

_{f(p)}c' always implies g(c) ≤

_{p}g(c'). Now the appropriate notion of

__Pref__-ballot is the functor F ∈

__Bal__

_{Pref}that takes n to the set of all rankings of n candidates, where the order ≤

_{i}is defined by R ≤

_{i}R' iff R' resulted from taking R and just moving candidate i up some number of spots and leaving everyone else the same.

Now just the fact that sc has to output arrows in

__Pref__means that it must be monotone; if across society, we only improve the opinion of candidate i, then the social choice should only have a better opinion of i.

So I think Arrow's theorem is the fact that the only left inverses to Δ : F → F

^{m}:

__FinOrd__

^{op}→

__Pref__are projections.