---
tag: N84M16W19X
kind: statement
role: theorem
name: Lawvere's fixed-point theorem
msc: [18D15, 03G30, 18A15]
uses: [BFBNQ36QS8, RHWD8DY41R, EK85VSSRMR, S5744QZV4N, 0XCH8QVDCQ, 0WTEMGYV2C]
about: [BFBNQ36QS8]
sources:
  - url: https://en.wikipedia.org/wiki/Lawvere%27s_fixed-point_theorem
same_as:
  wikidata: Q15809744
  wikipedia: Lawvere's fixed-point theorem
---

## Statement

Let $\mathcal{C}$ be a [[Cartesian closed category|BFBNQ36QS8]] with [[terminal object|EK85VSSRMR]] $1$.
A *point* of an object $X$ is a morphism $1 \to X$.
Let $A$ and $B$ be objects, and let $B^A$ be the [[exponential object|RHWD8DY41R]].
Let $\phi \colon A \to B^A$ be point-surjective: for every point $q \colon 1 \to B^A$ there is a point $p \colon 1 \to A$ with $\phi \circ p = q$.
Then every morphism $f \colon B \to B$ has a fixed point: there is a point $s \colon 1 \to B$ with $f \circ s = s$.

## 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|S5744QZV4N]].
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|0WTEMGYV2C]] that no set maps onto its power set.
The proof is an abstract form of [[Cantor's diagonal argument|0XCH8QVDCQ]].

## Explanations

### L1 human

Suppose the elements of a set $A$ can serve as codes for all functions from $A$ to $B$.
Then every map from $B$ to itself must leave some value unchanged.
Flipping a bit leaves no value unchanged, so no set can code all bit-valued functions on itself.
This one short argument is behind Cantor's theorem and Russell's paradox.

### L2 human

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.