# Fixed Points, Part 1: What is a Fixed Point?

A fixed point of a function is an input the function maps to itself. When we study the fixed points of a function, we can learn many interesting things about the function itself. This first of four parts defines fixed points, and looks at a few examples.

## What is a fixed point?

A fixed point of a function `f`

is some object `x`

so that

f x = x

- Gaiane
- Why does the equation you wrote,
`f x = x`

, make sense? - Plautus
- I say it does make sense. For we require that
`f`

is a function, so we can write`f x`

, and of course we can test for equality, so we can write`f x = x`

. - Gaiane
- But not every object is a valid input to
`f`

. We cannot, for example, discuss what would happen if we incremented a body of water, since bodies of water are not numbers. - Plautus
- Indeed, this seems to be a mistake…

Then we say that a fixed point of a function `f`

is some object `x`

, which is a valid input for `f`

, for which

f x = x

- Gaiane
- I agree now that
`f x`

makes sense. But does the equality test make sense? - Plautus
- Certainly! Two objects are equal or they are not; it is as simple as that.
- Gaiane
- Would you say that Stravinsky’s
*Rite of Spring*is either equal to the concept of justice, or it is unequal? - Plautus
- I would say it is unequal. For the
*Rite of Spring*is a musical composition, and justice is a concept. And things that are different in kind must be different in fact. - Gaiane
- I suppose this is reasonable. Nonetheless, I am bothered by the possibility of comparing two things that are different in kind.
- Plautus
- I understand. Perhaps the theory of types can clarify.

Suppose we can compare objects of type `α`

. Then we can say that some `x : α`

is a fixed point of `f : α → α`

, if

f x = x

In other words, we define

x “is fixed point of” f ≡ (f x = x)

## Are there fixed points?

- Gaiane
- I am satisfied with this definition. But is it empty? Are there
`α`

that can be compared, objects`x : α`

, and functions`f : α → α`

? - Plautus
- I endeavor to demonstrate that there are, so:

There are `α`

which can be compared. For consider the type `1`

, which has the single element `⋆`

. Objects of this type can be compared, where they are always equal. Furthermore, if we consider sums `α + β`

and pairs `α × β`

of comparable types, these types too are comparable. And finally, an inductive type (of which more later) is also comparable. This gives us quite a rich universe of types which are comparable. [1]

There are objects `x : α`

. In fact, the type `1`

is inhabited (by `⋆`

), and so are sums and pairs and some inductions of inhabited types. Thus we have quite a rich universe even of comparable, inhabited types.

Finally, there are functions `f : α → α`

. For there exists at least the identity function `id : ∏ α · α → α`

, and for some `α`

there may exist others.

Thus the study of the fixed points of functions is not vacuous.

## A demonstration

- Gaiane
- In this case, can you demonstrate a fixed point?
- Plautus
- Certainly. First, I will demonstrate a simple example.

Consider the type `1`

, which is comparable. Then consider `x ≡ ⋆ : 1`

and the function `f ≡ id₁ : 1 → 1`

. It is true that `f x ≡ id₁ ⋆ ≡ ⋆ ≡ x`

, so that `⋆`

is a fixed point of `id₁`

.

There are functions which are not the identity, which also have fixed points. Consider the type `1 + 1`

, which is comparable. Then consider `x ≡ lft ⋆ : 1 + 1`

, and `f : 1 + 1 → 1 + 1`

defined by

f (lft a) ≡ (lft a) f (rgt a) ≡ (lft a)

Then `x`

is a fixed point of `f`

.

Also consider the function `id₁₊₁ : 1 + 1 → 1 + 1`

. Both `lft ⋆`

and `rgt ⋆`

are its fixed points.

Finally, consider the function `g : 1 + 1 → 1 + 1`

defined by

g (lft a) = (rgt a) g (rgt a) = (lft a)

`g`

does not have a fixed point.

- Gaiane
- So the study of fixed points has content, and there are functions with no fixed points, and functions with fixed points one and several.

[1] A rigorous and beautiful treatment of equality in abstract type theory is given in Homotopy Type Theory, which you can read for free.