This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Fixed points of endofunctions

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)