Is there a "mind-blowing fact" about category theory? Like the first time I've heard that one can prove there is no analytical solution for a polynomial equation with a degree > 5 with group theory, it was mind-blowing. What's the counterpart of category theory?

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

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).

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.