A Survey on Lawvere's Fixed-Point Theorem
Joaquim Reizi Barreto
TL;DR
The paper analyzes Lawvere's Fixed-Point Theorem, which guarantees fixed points in Cartesian Closed Categories under a point-surjective morphism, thereby formalizing self-reference. The method builds from foundational notions including terminal objects, products, exponential objects, evaluation maps, currying, and point-surjective morphisms, and proves the theorem via the Universality of Currying and the Diagonal Lemma, followed by the Fixed-Point Construction Lemma. It surveys applications to fixed-point combinators in programming, and to type theory and homotopy type theory, including connections to Univalent Foundations and Higher Topos Theory, and discusses open problems. Overall, the work provides a unified categorical perspective on self-reference, supported by diagrammatic intuition that links classical diagonal arguments to modern foundations.
Abstract
This paper provides an overview of Lawvere's Fixed-Point Theorem in category theory and aims to detail the universal framework underlying self-reference and recursive structures. First, we rigorously define fundamental concepts - such as terminal objects, products, Cartesian Closed Categories, exponential objects, evaluation maps, currying, and point-surjective morphisms - and explain their intuitive meanings through concrete examples and commutative diagrams. Based on these foundational notions, we derive key lemmas (the universality of currying, the diagonal lemma, and the fixed-point construction lemma) and integrate them to develop a proof of Lawvere's Fixed-Point Theorem. Furthermore, we discuss the impact of this theorem on fixed-point combinators in programming languages, type theory, and homotopy type theory, as well as current research trends and open problems. In doing so, we clarify how the abstract principle of self-reference contributes to a wide range of applications in both mathematics and computational theory.