[Lawvere's fixed point theorem][1] states that in a [cartesian closed category][2], if there is a morphism $A \to X^A$ which is [point][3]-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][4] for an expository account. Somehow it reminds me of the Yoneda 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][5] alludes to it). *Edit.* Since March '14 there is an [nlab entry][6].
 
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?

Qiaochu [recently asked][7] if the theorem implies [Brouwer's fixed point theorem][8]. 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 $G\mathsf{-Set}$ for a group $G$ (here, a point of a $G$-set is already fixed by the $G$-action), the category $\mathrm{Sh}(X)$ of sheaves on a space $X$ (here a point is a global section), or the category of compactly generated (weak) Hausdorff spaces $\mathsf{CGHaus}$. What are interesting choices for the object $A$, and how can we use the resulting fixed point theorem?


  [1]: http://www.tac.mta.ca/tac/reprints/articles/15/tr15abs.html
  [2]: http://en.wikipedia.org/wiki/Cartesian_closed_category
  [3]: http://ncatlab.org/nlab/show/global+element
  [4]: http://arxiv.org/pdf/math/0305282.pdf
  [5]: http://ncatlab.org/nlab/show/Cantor%27s%20theorem
  [6]: http://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem
  [7]: http://mathoverflow.net/questions/136478
  [8]: http://en.wikipedia.org/wiki/Brouwer_fixed-point_theorem