Lawvere's fixed-point theorem

In mathematics, Lawvere's fixed-point theorem is an important result in category theory.

[1] It is a broad abstract generalization of many diagonal arguments in mathematics and logic, such as Cantor's diagonal argument, Cantor's theorem, Russell's paradox, Gödel's first incompleteness theorem, Turing's solution to the Entscheidungsproblem, and Tarski's undefinability theorem.

[2] It was first proven by William Lawvere in 1969.

[3][4] Lawvere's theorem states that, for any Cartesian closed category

in it, if there is a weakly point-surjective morphism

to the exponential object

The theorem's contrapositive is particularly useful in proving many results.

which has no fixed points, then there is no object

with a weakly point-surjective map