Scott Aaronson, in this funny April Fools’ Day post, introduces a fictionalized $P \neq NP$ Proof and, among other things, he says that the proof make use of
Higher topos theory to solve the biggest problem there was.
More and more often I hear about Category Theory (of which the former Higher Topos Theory is part) . Some say it is one of the branches of pure mathematics that is undergoing the most dramatic developments in recent years (some say it will replace set theory as the foundation of mathematics), while others are still a bit skeptical.
I am not aware of an extensive use in Computer Science, but (it seems that) it is becoming more and more present (functional programming, type theory, data structures, etc.). Furthermore, I do not believe that Scott Aaronson mentioned it at random as a tool used for a possible proof of $P \neq NP$: the bird eye view it provides on mathematical and logical entities could be extremely important and help us to identify some common properties that we have never been able to see because we lacked the right tools.
My question is the following: have there been researchers who have achieved important results in the field of computational complexity using the tools of category theory? How do theoretical computer scientists see this theory?
