Fixed points of endofunctions

Content created by Fredrik Bakke.

Created on 2024-04-17.
Last modified on 2024-04-17.

module foundation.fixed-points-endofunctions where
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.identity-types


Given an endofunction f : A → A, the type of fixed points is the type of elements x : A such that f x = x.


module _
  {l : Level} {A : UU l} (f : A  A)

  fixed-point : UU l
  fixed-point = Σ A  x  f x  x)

  fixed-point' : UU l
  fixed-point' = Σ A  x  x  f x)

Recent changes