nLab anafunction

Anafunctions

Anafunctions

Idea

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”.

In homotopy type theory

In dependent type theory (homotopy type theory), an anafunction is a type family RR indexed by types AA and BB such that for each element a:Aa \colon A, the dependent sum type b:BR(a,b)\sum_{b \colon B} R(a, b) is a contractible type:

isAnafunction(R) a:AisContr( b:BR(a,b)). \mathrm{isAnafunction}(R) \;\coloneqq\; \prod_{a:A} \mathrm{isContr} \left( \sum_{b \colon B} R(a, b) \right) \,.

Since the principle of unique choice holds in dependent type theory, it follows that given any anafunction a:A,b:BR(a,b)typea\colon A, b \colon B \vdash R(a, b) \; \mathrm{type}, there is a function a:Af(a):Ba \colon A \vdash f(a) \colon B.

The categorical semantics of an anafunction in homotopy type theory is an \infty -anafunctor, since the identity types between two elements of a type are not required to be mere propositions.

Given any type family RR indexed by types AA and BB, there is a type family R opR^\op indexed by BB and AA, defined by R op(b,a)R(a,b)R^\op(b, a) \coloneqq R(a, b) for all aconAa \con A and b:Bb \colon B. An anafunction RR is an equivalence of types if both RR and R opR^\op are anafunctions.

 See also

 References

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.