@ John Baez:
I had a thought. I know you can use the Lawvere fixed point theorem to prove the halting problem. Generalized to Oracle machines, it establishes separation theorems for the [Arithmetical hierarchy](https://en.wikipedia.org/wiki/Arithmetical_hierarchy).
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?
On a related not, it's well known that the fixed point theorem can be used to prove Gödel's first incompleteness theorem. However, 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...