Lawvere's fixed-point theorem

Remarks

Proof idea: let $\mathrm{ev} \colon B^A \times A \to B$ be evaluation and $\Delta \colon A \to A \times A$ the diagonal, built from the product. Put $g = f \circ \mathrm{ev} \circ (\phi \times \id_A) \circ \Delta \colon A \to B$, so that informally $g(a) = f(\phi(a)(a))$. The transpose of $g$ is a point of $B^A$, so it equals $\phi \circ p$ for some point $p$ of $A$. Then $s = g \circ p$ satisfies $s = f(\phi(p)(p)) = f(g(p)) = f \circ s$.

The contrapositive is the form used most. In $\mathbf{Set}$, take $B = \set{0, 1}$ and $f$ the swap of $0$ and $1$, which has no fixed point. So no map $A \to \set{0,1}^A$ is surjective, which is Cantor's theorem that no set maps onto its power set. The proof is an abstract form of Cantor's diagonal argument.

Going deeper

For a student

The theorem needs only finite products and exponentials, so it applies in any Cartesian closed category, including toposes and models of the typed lambda calculus. Read positively, it explains fixed-point combinators: if $A$ maps point-surjectively onto $A^A$, then every endomorphism of $A$ has a fixed point. Read negatively, it unifies diagonal arguments: Cantor's theorem, Russell's paradox and Tarski's undefinability of truth all come from an $f$ without fixed point that forbids a point-surjection.