Lawvere's fixed point theorem
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.
Created on 2022-02-09.
Last modified on 2024-04-11.
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)
Recent changes
- 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2023-12-21. Fredrik Bakke. Action on homotopies of functions (#973).
- 2023-10-22. Egbert Rijke and Fredrik Bakke. Refactor synthetic homotopy theory (#654).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644).