Matthew wrote:

> I am wondering: can the separation theorems for the time and space hierarchies in ordinary complexity theory also be seen as applications of the Lawvere fixed point theorem?

I don't have the combination of time and space (= brainpower) to answer this. For example, I have no clue as to how people _usually_ prove those separation theorems. However, if someone were able to prove these theorems using the Lawvere fixed point theorem, that would be a nice (small) step toward applying category theory to computational complexity.

There's a famous divide between the computer scientists who like category theory and those who like computational complexity. Any step toward bridging this divide would be great.

> I found a super cute proof that applies it to prove the _second_ incompleteness theorem rather succinctly. Not sure if it's something to post here...

Cool! Is this really new? If so, it might be better to post it on the \\(n\\)-Category Café and/or the Azimuth blog. That way, more people would see it. If you post it here, I can repost it there, as a "guest post".