"One of the first things to learn about category theory is that not everything in mathematics is a category"

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.