The Categorical Imperative — Tiny Revelations, Massive Abstractions (Dr. Katya Steiner)
# The Categorical Imperative — Tiny Revelations, Massive Abstractions
If you still think category theory is only for people who enjoy abstract misery, congratulations: you are exactly the person I want to convince. Not by ritual initiation, not by reciting Mac Lane like catechism, but by the thing that keeps grad students awake at 3 a.m. with a stupid grin — the tiny revelation. That one diagram that suddenly looks clean. The lemma that recasts an ugly proof as a picture. The monad that, after a week of resentment, finally feels like a projection.
Let’s be clear: category theory is equal parts taste and tooling. It’s a style of thinking that translates across disciplines. So here’s a practical, slightly opinionated reflection on how to love it, use it, and not be an asshole about it.
## Celebrate the small wins
Big theorems are sexy; micro-joys are sustainable. A clearer diagram, a shorter counterexample, or a canonical factorization you didn’t expect — these are the carburators of long-term engagement. Write them down. Tweet them. Post them to Slack or your department mailing list. Making an intuition communicable forces you to sharpen it.
From a cognitive-science angle this matters: representation changes reasoning. Once you can sketch a long exact sequence, a universal property, or a pullback in your head, you stop chasing symbols and start seeing structure. That’s where real problem-solving lives.
## Catalogue, curate, and stop reinventing the syllabus
Two lists will save you: canonical texts (Mac Lane, Riehl, Awodey) and hyper-specific monographs that nail a single problem. Add surveys, useful blog posts, and a few repos. When you’re writing code or reading a thesis late at night, your curated list is sanity.
Also collect the oddities: papers that feel like they solve a problem once and perfectly. Those weird gems are often where cross-disciplinary ideas come from.
## Make abstraction do something tangible
You’ll learn fastest by forcing abstract machinery to behave on concrete puzzles. Topology gives a beautiful set of examples: ultrafilters and compact Hausdorff spaces. The ultrafilter functor β on Set can be terrifying in the abstract, but think of it as a device for “ways to converge.” In a compact Hausdorff X, every ultrafilter has a unique limit. Working through finite discrete sets (only principal ultrafilters), Stone–Čech of ℕ (a zoo), and [0,1] (many ultrafilters collapse to the same point) turns the monster into a set of sensible behaviors.
Another cross-section: in measure theory, consider the relationship between sigma-algebras and Boolean algebras — the categorical viewpoint helps you see how morphisms preserve or reflect structure, and when not to expect nice adjoints.
Pro tip: when you see “ultrafilters of ultrafilters” or higher iterates, translate to limits, convergences, and images. Concretize first, then re-abstract.
## Ologs: duct tape for modeling reality (with tests)
Ologs (ontology logs) are delightful: types as boxes, aspects as arrows. But they’re furniture unless you attach instances. Treat an olog like a schema: build minimal instances in a spreadsheet, JSON, or a tiny graph DB. If an aspect fails for your example data, it’s not a theorem — it’s a bad model.
Two practical patterns:
– Prototyping: Minimal instances in CSV/JSON let you find mismatches fast.
– Tooling: Couple a diagram editor with a validation layer (scripts, or libraries that treat diagrams as schemas).
Diagrams without data are pretty. Diagrams with tests are useful. Spend your time on the latter.
## When μ feels like a projection (and why that’s satisfying)
Sometimes the abstract machinery collapses into something deliciously concrete. Take a monad T = (T, η, μ) on C and a linearization functor L : C → Vect. Certain composites of η and μ may become idempotent in Vect. Idempotents that split correspond to projections after passing to the Karoubi envelope. In practice this means μ can behave like a projection onto an image subspace.
A student formalizing this in Lean observed exactly that: L(η ∘ μ) is an idempotent e; splitting e gives an inclusion and projection. Suddenly a monad that once felt like philosophical flab is a computable linear operator. For the state monad the intuition is great: one map duplicates state, another discards it — their composite is projection-like. This is the kind of clarity that turns folklore into code and slides into a neat repo.
## Cross-pollination: logic, type theory, and CS
Category theory is the lingua franca between type theory, model theory, and programming-language semantics. Toposes encode internal logic; cartesian closed categories talk to simply typed lambda calculus; monads show up as side-effects in Haskell and as semantic clarifiers in denotational semantics. From proof theory, the Curry–Howard correspondence gets recast categorically: proofs are morphisms, propositions are objects.
But balance: not every categorical insight is the Swiss Army knife it pretends to be. Formalizing something in a proof assistant may take months for a one-line insight. Sometimes the overhead of categorical machinery is heavier than the problem demands. Recognize when brevity and hands-on computation beat the most elegant universal property.
## When people grumble — and when they’re right
There’s a valid grumble that category theory can become cathedral-building: elegant universals that answer questions you never asked. The antidote is practice. If your abstraction helps you simplify, compute, or model — keep it. If it’s an ornament for an already-sprung leak, be suspicious.
Also: “folklore” exists for a reason. Many neat pictures are already known. That doesn’t make your rephrasing worthless. Clarity is a public good.
## Takeaways (quick, selfish list)
– Chronicle micro-insights; they compound.
– Maintain a readable catalogue of long-form resources.
– Force abstractions to behave on concrete examples (ultrafilters, monads, toposes).
– When modeling, attach instances and automated checks.
– Formalize the moments where intuition meets algebra — even if they’re folklore.
Category theory isn’t a rite of passage. It’s a toolbox. Use it to simplify, model, and take a little dishonest joy when a messy system snaps into a tidy diagram.
So here’s the last, slightly smug question: what tiny categorical picture changed how you think about a whole class of problems — and are you willing to write a two-page repo that makes the rest of us look smarter for ten minutes?