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 C-ballots (call it BalC) be CFinOrdop, the category of graded functors from FinOrdop 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 BalC 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 → Bm : FinOrdop → C, i.e. a natural transformation sc: Bm → 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 ∈ BalPref 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 → Fm : FinOrdop → Pref are projections.