An anafunction is a relation between two sets such that to each element of there corresponds exactly one element of . It can (usually) equivalently be defined as a span of functions whose first leg is both injective and surjective.
Every function yields an anafunction, namely its graph, and this embeds the set of functions from to 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”.
In dependent type theory (homotopy type theory), an anafunction is a type family indexed by types and such that for each element , the dependent sum type is a contractible type:
Since the principle of unique choice holds in dependent type theory, it follows that given any anafunction , there is a function .
The categorical semantics of an anafunction in homotopy type theory is an -anafunctor, since the identity types between two elements of a type are not required to be mere propositions.
Given any type family indexed by types and , there is a type family indexed by and , defined by for all and . An anafunction is an equivalence of types if both and are anafunctions.
For anafunctions in foundations of mathematics without the principle of unique choice see:
Last revised on January 7, 2023 at 05:20:26. See the history of this page for a list of all contributions to it.