Anafunctor

Template:Short description Template:Wiktionary An anafunctorTemplate:Refn is a notion introduced by Template:Harvtxt for ordinary categories that is a generalization of functors.Template:R In category theory, some statements require the axiom of choice, but the axiom of choice can sometimes be avoided when using an anafunctor.^[1] 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.Template:R^[2]

Definition

Let Template:Mvar and Template:Mvar be categories. An anafunctor Template:Mvar with domain (source) Template:Mvar and codomain (target) Template:Mvar, and between categories Template:Mvar and Template:Mvar is a category $| F |$ , in a notation $F : X \overset{a}{\to} A$ , is given by the following conditions:^[3]^[4]^[5]^[6]^[7]

Let pair $F_{0} : | F | \to X$ and $F_{1} : | F | \to A$ be functors, a span of ordinary functors ( $X \leftarrow | F | \to A$ ), where $F_{0}$ is fully faithful.

An anafunctor $F : X \overset{a}{\to} A$ following condition:Template:R^[8]^[9]

A set $| F |$ of specifications of $F$ , with maps $σ : | F | \to O b (X)$ (source), $τ : | F | \to O b (A)$ (target). $| F |$ is the set of specifications, $s \in | F |$ specifies the value $τ (s)$ at the argument $σ (s)$ . For $X \in O b (X)$ , we write $| F | X$ for the class ${s \in | F | : σ (s) = X}$ and $F_{s} (X)$ for $τ (s)$ the notation $F_{s} (X)$ presumes that $s \in | F | X$ .
For each $X, Y \in O b (X)$ , $x \in | F | X$ , $y \in | F | Y$ and $f : X \to Y$ in the class of all arrows $A r r (X)$ an arrows $F_{x, y} (f) : F_{x} (X) \to F_{y} (Y)$ in $A$ .
For every $X \in O b (X)$ , such that $| F | X$ is inhabited (non-empty).
$F$ hold identity. For all $X \in O b (X)$ and $x \in | F | X$ , we have $F_{x, x} ({i d}_{x}) = {i d}_{F_{x} X}$
$F$ hold composition. Whenever $X, Y, Z \in O b (X)$ , $x \in | F | X$ , $y \in | F | Y$ , $z \in | F | Z,$ and $F_{x, z} (g f) = F_{y, z} (g) \circ F_{x, y} (f)$ .