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

In ordinary mathematics the set of anafunctions from $A$ to $B$ is either literally the same as, or isomorphic to, the set of functions from $A$ to $B$, and so 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”.

Created on November 21, 2017 at 02:33:09.
See the history of this page for a list of all contributions to it.