Lawvere's fixed point theorem

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

Created on 2022-02-09.
Last modified on 2023-06-08.

module foundation.lawveres-fixed-point-theorem where
Imports 
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.propositional-truncations
open import foundation.surjective-maps
open import foundation.universe-levels

open import foundation-core.function-extensionality
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

abstract
  fixed-point-theorem-Lawvere :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → A → B} →
    is-surjective f → (h : B → B) → ∃ B (λ b → h b ＝ b)
  fixed-point-theorem-Lawvere {A = A} {B} {f} H h =
    apply-universal-property-trunc-Prop
      ( H g)
      ( ∃-Prop B (λ b → h b ＝ b))
      ( λ p → intro-∃ (f (pr1 p) (pr1 p)) (inv (htpy-eq (pr2 p) (pr1 p))))
    where
    g : A → B
    g a = h (f a a)

Recent changes