Anafunctor

In mathematics, an anafunctor is a notion introduced by for ordinary categories that is a generalization of functors. In category theory, some statements require the axiom of choice, but the axiom of choice can sometimes be avoided when using an anafunctor. For example, the statement "every fully faithful and essentially surjective functor is an equivalence of categories" is equivalent to the axiom of choice, but we can usually follow the same statement without the axiom of choice by using anafunctor instead of functor.

Definition

Span formulation of anafunctors

Let and be categories. An anafunctor with domain and codomain, and between categories and is a category, in a notation, is given by the following conditions:

is surjective on objects.
Let pair and be functors, a span of ordinary functors, where is fully faithful.

Set-theoretic definition

An anafunctor following condition:

A set of specifications of, with maps, . is the set of specifications, specifies the value at the argument. For, we write for the class and for the notation presumes that.
For each,, and in the class of all arrows an arrows in.
For every, such that is inhabited.
hold identity. For all and, we have
hold composition. Whenever,,, and.