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
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.identity-types

Idea

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

Definitions

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

  fixed-point : UU l
  fixed-point = Σ A (λ x → f x ＝ x)

  fixed-point' : UU l
  fixed-point' = Σ A (λ x → x ＝ f x)

Recent changes