An anafunction is a relation between two sets A,BA,B such that to each element of AA there corresponds exactly one element of BB. It can (usually) equivalently be defined as a span AFBA \leftarrow F \to B of functions whose first leg FAF\to A is both injective and surjective.

Every function yields an anafunction, namely its graph, and this embeds the set of functions from AA to BB into the set of anafunctions. Conversely, in ordinary mathematics every anafunction is the graph of some function, so these two sets are isomorphic (and indeed, in some foundations such as material set theory, equal). Thus in such cases the notion of anafunction is unneeded.

However, in more exotic contexts where the function comprehension principle? (a.k.a. the “axiom of unique choice”) fails, such as the internal logic of a quasitopos or a tripos, it may be necessary to distinguish anafunctions from functions. Indeed, the fact that every anafunction is a function, or equivalently that every injective and surjective function is an isomorphism, is essentially the definition of the function comprehension principle.

Anafunctions are a decategorification of the notion of anafunctor, and take their name from the latter. Traditionally they would be called “total functional relations”.

Last revised on April 27, 2019 at 10:55:06. See the history of this page for a list of all contributions to it.