Had a thought in the shower this morning about the fact that the free commutative monoid monad isn't cartesian — something I had got really bummed about since finding it out yesterday. I think I understand better now that to use it for the context-structure monad would be like having a sequent where things were so deeply commutative that you couldn't even tell one hypothesis of proposition A from another: as if you didn't even have labels or variable names or anything. Now while this would still work just as well for raw provability in place of real proof theory (parallel to the vanishing of all concerns about the monad being cartesian (i.e. preserving pullbacks and having natural transformations whose naturality diagrams are pullbacks) if we were working with just posets and not categories) of course our notion of proof would be fucked up if different hypotheses were totally indistinguishable up to permutation, i.e. if variables didn't have names.
Instead, we give them names, and understand that there is an exchange property or rule, for which we might have to do some real work like swapping around deBruijn indices when we perform it. Once again my problems are due to the forgetting the Fundamental Lesson of Weak n-Category Theory, to wit,
don't think things need to be identical when they merely need to be isomorphic