Lawvere's fixed point theorem states that in a cartesian closed category, if there is a morphism $A \to X^A$ which is point-surjective (meaning that $\hom(1,A) \to \hom(1,X^A)$ is surjective), then every endomorphism of $X$ has a fixed point (meaning a morphism $1 \to X$ which is fixed by the endomorphism). It unifies several (all?) diagonal arguments appearing in mathematical logic (Cantor's theorem, Russel's paradox, Tarski's non-definability of truth, the Recursion theorem, Gödel's first incompleteness theorem). See Yanovsky's paper for an expository account. Somehow it reminds me of Yoneda's Lemma, because the proof is so short and simple, but the theorem unifies several theorems which are often regarded to be nontrivial. I wonder why it doesn't have a Wikipedia or at least an nlab entry yet (only Cantor's theorem alludes to it).
The applications mentioned above all take place within the category of sets (or similar categories). But since the theorem applies to arbitrary cartesian closed categories, I wonder:
Question. Are there any interesting applications of Lawvere's fixed point theorem outside of mathematical logic by applying it to cartesian closed categories which are substantially different from the category of sets?
Recently Qiaochu asked if the theorem implies Brouwer's fixed point theorem, but this seems to be a little bit too optimistic. Anyway, it would be nice to see at least some applications. Interesting examples of cartesian closed categories include the category of $G$-sets for a group $G$ (here, a point of a $G$-set is already fixed by the $G$-action), the category sheaves on a space (here a point is a global section), or the category of compactly generated (weak) Hausdorff spaces. What are interesting choices for the object $A$, and how can we use the resulting fixed point theorem?