strongly extensional function

Strongly extensional functions


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.


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

Let XX and YY be sets, each equipped with a tight apartness \ne. Let ff be a function from XX to YY. Then ff is strongly extensional if aba \ne b whenever f(a)f(b)f(a) \ne f(b).

Note that if ff 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 ff 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 ff is also strongly extensional. In this way, strong extensionality is a constructively stronger but classically equivalent variation of extensionality.

We have a category Set 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 Set Set_{\ne}, the monomorphisms being merely injective in the usual sense of reflecting equality.)


If XX has decidable equality, then the negation of equality is a (in fact the unique) tight apartness on XX, and any function from XX to any set YY (with any tight apartness on YY) 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 𝕀\mathbb{I}, where an internal real number is (externally) a continuous map from 𝕀\mathbb{I} to the real line \mathbb{R}, consider the internal number cc given by the function (ttt 2)(t \mapsto t - t^2). Then the subspace {0,c}\{0,c\} of the internal real line is an internal complete metric space (as proved by Richman), we may define an internal continuous map f:{0,c}f\colon \{0,c\} \to \mathbb{R} by f(0)=0f(0) = 0 and f(c)=1f(c) = 1, and of course we have f(0)f(c)f(0) \ne f(c) internally. But the internal truth value {0c}\{0 \ne c\} is only the open interval ]0,1[]0,1[, not all of [0,1][0,1], so it's not completely true that ff is strongly extensional. (However, this ff is not not strongly extensional, so a stronger counterexample would be nice.)


Last revised on March 3, 2013 at 13:53:48. See the history of this page for a list of all contributions to it.