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
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).