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.

In ordinary mathematics the set of anafunctions from AA to BB is either literally the same as, or isomorphic to, the set of functions from AA to BB, 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.