# Strongly extensional functions

## Idea

In constructive mathematics, one sometimes calls a function ‘extensional’ to stress that it preserves equality (as opposed to a prefunction, which need not do so). A function is strongly extensional if it also reflects inequality in a relevant sense. One usually employs this in a context where the principle of excluded middle is enough to prove that every function is strongly extensional.

## Definitions

This is probably not the only context where the term ‘strongly extensional’ is used, but it's the one that I know.

Let $X$ and $Y$ be sets, each equipped with a tight apartness $\ne$. Let $f$ be a function from $X$ to $Y$. Then $f$ is strongly extensional if $a\ne b$ whenever $f\left(a\right)\ne f\left(b\right)$.

Note that if $f$ is only a prefunction (in a foundation where this makes sense) and we impose the condition of strong extensionality, it follows (upon taking the contrapositive?, since equality is the negation of any tight apartness) that $f$ is extensional (and so a function). Conversely, if $\ne$ is also the negation of equality (which is always the unique tight apartness in classical mathematics), then any extensional $f$ is also strongly extensional. In this way, strong extensionality is a constructively stronger but classically equivalent variation of extensionality.

We have a category ${\mathrm{Set}}_{\ne }$ whose objects are sets equipped with tight apartnesses and whose morphisms are strongly extensional functions.

A strongly extensional function is strongly injective if it also preserves $\ne$. (These are the regular monomorphisms of ${\mathrm{Set}}_{\ne }$, the monomorphisms being merely injective in the usual sense of reflecting equality.)

## Examples

If $X$ has decidable equality, then the negation of equality is a (in fact the unique) tight apartness on $X$, and any function from $X$ to any set $Y$ (with any tight apartness on $Y$) must be strongly extensional.

Any pointwise-continuous function between metric spaces is strongly extensional. Using countable choice and Markov's principle (or actually weak versions thereof), it follows that any function to a metric space from a complete metric space (regardless of continuity!?) is strongly extensional.

A weak counterexample: Internal to the topos of sheaves on the unit interval $𝕀$, where an internal real number is (externally) a continuous map from $𝕀$ to the real line $ℝ$, consider the internal number $c$ given by the function $\left(t↦t-{t}^{2}\right)$. Then the subspace $\left\{0,c\right\}$ of the internal real line is an internal complete metric space (as proved by Richman), we may define an internal continuous map $f:\left\{0,c\right\}\to ℝ$ by $f\left(0\right)=0$ and $f\left(c\right)=1$, and of course we have $f\left(0\right)\ne f\left(c\right)$ internally. But the internal truth value $\left\{0\ne c\right\}$ is only the open interval $\right]0,1\left[$, not all of $\left[0,1\right]$, so it's not completely true that $f$ is strongly extensional. (However, this $f$ is not not strongly extensional, so a stronger counterexample would be nice.)

## References

Revised on March 3, 2013 13:53:48 by Toby Bartels (98.16.160.142)