Thanks, interesting!

Thanks to MO's "Related"-feature I realized that this question has already been answered here: mathoverflow.net/questions/36766/… (2/2)

In a previous version of my post I asked whether the theorem above can be formulated as an equivalence between the category of algebras over the monad induced by the adjunction and the category of coalgebras over the comonad induced by the adjunction (this was motivated by the fact that this holds for adjunctions between posets, in which case the algebras and coalgebras turn out to be the same as the fixed points $P'$ and $Q'$). (1/2)

@PaulTaylor I see, thanks. However, given the adjunction between topological spaces and locales and the goal to restrict this adjunction to an equivalence between full subcategories, how do you get the idea to consider sober spaces and spatial locales "by hand", i.e., without knowing the above theorem. Isn't the whole task much easier when one knows that it's useful to consider the objects for which the unit/counit is an isomorphism?

@MarcOlschok Indeed, thanks!

@PaulTaylor Thanks. But I don't agree that just because a statement has an easy or even trivial proof it is a poor theorem. (Your comment somehow suggests this viewpoint.)

That's remarkable: I just looked into Mac Lane's CWM for reference of the above theorem but it seems it isn't in there!

Googling "profunctor" I haven't found a text that explains how profunctors induce adjunctions in the same way that relations induce Galois connections. Concerning 3: I haven't computed any examples. My hope is that the answer to this question is well-known among category theorists. Concerning 4: I agree that it is a soft question. But it would be helpful if an expert could just tell me "I used the theorem to prove an equivalence result I wouldn't have discovered without the theorem" or "In my experience nearly all equivalence results arise without the theorem".