I can't imagine that Boolos used Lawvere's fixed point theorem to prove Gödel's second incompleteness theorem! He may have used a fixed point argument that you can instantly recognize as a special case of Lawvere's fixed point theorem. But making that explicit would be a great \\(n\\)-Café post... as long as you admit that it's not utterly brand new. People there like seeing things done with categories!

> In the case of computational complexity theory, I am not sure if diagonalization is taking place in a CCC with a suitable epimorphism.

It would be very nice to get CCC's for different complexity classes of functions.

> In the case of computational complexity theory, I am not sure if diagonalization is taking place in a CCC with a suitable epimorphism.

It would be very nice to get CCC's for different complexity classes of functions.