# Lawvere's fixed point theorem

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-02-09.

module foundation.lawveres-fixed-point-theorem where

Imports
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.function-extensionality
open import foundation.propositional-truncations
open import foundation.surjective-maps
open import foundation.universe-levels

open import foundation-core.identity-types


## Idea

Lawvere's fixed point theorem asserts that if there is a surjective map A → (A → B), then any map B → B must have a fixed point.

## Theorem

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → A → B}
where

abstract
fixed-point-theorem-Lawvere :
is-surjective f → (h : B → B) → exists-structure B (λ b → h b ＝ b)
fixed-point-theorem-Lawvere H h =
apply-universal-property-trunc-Prop
( H g)
( exists-structure-Prop B (λ b → h b ＝ b))
( λ (x , p) → intro-exists (f x x) (inv (htpy-eq p x)))
where
g : A → B
g a = h (f a a)