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

Separation for time and space complexity hierarchies is proved by a kind of diagonalization (see [Arora and Barak (2007), §3, pgs. 65-74](http://theory.cs.princeton.edu/complexity/book.pdf))

Similar diagonalization arguments also crop up in descriptive set theory for establishing higher separation theorems. For nice proof of this, I like [Jech (2003)](https://link.springer.com/book/10.1007%2F3-540-44761-X#about) where in chapter 11 he shows \$$\mathbf{\Sigma}^0_\alpha\neq \mathbf{\Pi}^0_\alpha\$$ (Corollary 11.3).

In the case of computational complexity theory, I am not sure if diagonalization is taking place in a CCC with a suitable epimorphism. However, I am much more confident that descriptive set theory is following the usual recipe.

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

Nah it's in Boolos' *The Logic of Provability* (1995). I can't find the citation but I think he got it from Martin Löb's writings in the 1950s. Unlike the first incompleteness theorem, the quick proof of the second incompleteness theorem applies the fixed point with some indirection á la [Curry's paradox](https://plato.stanford.edu/entries/curry-paradox/).

I'll try to post it in a *For Fun* thread.