Sorry, apologies, etc., for the long silence. I've been working on the final version of
a paper that I plan to post here in a few days. This mini-post is just to highlight an exchange on
MathOverflow that jibes with some things I've been thinking about lately. The quote in the title is from
Mike Shulman in response to
this question, "Why haven’t certain well-researched classes of mathematical object been framed by category theory?" I also like
Reid Barton's response, in particular, "From the standpoint of higher category theory, categories (i.e., 1-categories) are just one level among many in a family of mathematical structures". This seems to me like an important lesson to keep in mind when applying category theory to programming languages and proof theory: to resist the desire to phrase everything as a category.