A thing is its relationships. (Yoneda lemma.) Keep track of how an object connects to everything else, and you’ve recovered the object itself, up to isomorphism. It’s why mathematicians study things by probing them: a group by its actions, a space by the maps into it, a scheme in algebraic geometry defined as the rule for what maps into it look like. (You do need the full pattern of connections, not just a list — two different rings can have the same modules, for instance.) [0]

Writing a program and proving a theorem are the same act. (Curry–Howard–Lambek.) For well-behaved programs, every program is a proof of something and every proof is a program. The match is exact for simple typed languages and leaks a bit once you add general recursion (an infinite loop “proves” anything in Haskell), but the underlying identity is real. Lambek added the third leg: these are also morphisms in a category. [1]

Algebra and geometry are one thing wearing different costumes. (Stone duality and cousins.) A system of equations and the shape it cuts out aren’t related, they’re the same object seen from opposite sides. Grothendieck rebuilt algebraic geometry on this idea, with schemes (so you can do geometry on the integers themselves) and étale cohomology (topological invariants for shapes with no actual topology). His student Deligne used that machinery to settle the Weil conjectures in 1974. Wiles’s Fermat proof lives in the same world, though it leans on much more than the categorical foundations. [2]

[0] https://en.wikipedia.org/wiki/Yoneda_lemma

[1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[2] https://en.wikipedia.org/wiki/Stone_duality

well, this is more applied and less straightforwardly categorical, but thinking along the lines of solely looking at compositional structure rather than all the properties of functions we usually take as semantic bedrock in functional programming (namely referential transparency) is how you start doing neat arrowized tricks like tracking state in the middle of a big hitherto-functional pipeline (for instance automata, functions which return a new state/function alongside a value, can be neatly woven into pipelines composed via arrow composition in a way they can't be in a pipeline composed via function composition)

https://en.wikipedia.org/wiki/Abstract_nonsense

https://math.stackexchange.com/questions/823289/abstract-non...

Sometimes the proof in category theory is trivial but we have no lower dimension or concrete intuition as to why that is true. This whole state of affairs is called abstract nonsense.

Well, group theory is a special case of category theory. A group is a one object category where all morphisms are invertible. You do group theory long enough and it leads you to start thinking about groupoids and monoids and categories more generally as well.

I think that CT is more akin to just a different language for mathematics than a solid set of axioms from which you can prove things. The most fact-y proof I've personally seen was that you can't extend the usual definition of functions in set theory to work with parametric polymorphism (not that just some constructions won't work, but that there isn't one at all).

One of the most striking things is that cartesian products of objects do not correspond to set-cartesian products. This to me was mind-blowing when studying schemes.

Sure, category theory can't prove the unsolvability of the quintic. But did you know that a monad is really just a monoid object in the monoidal category of endofunctors on the category of types of your favorite language?

Just Yoneda Lemma. In fact it feels like the theory just restates Yoneda Lemma over and over in different ways.