Anafunctor

An anafunctor is a generalization of the notion of Functor that tends to work better in settings where the Axiom of Choice fails.

We can neatly define an anafunctor $F:\mathcal{C}\to\mathcal{D}$ as a span of categories $\mathcal{C}\leftarrow\overline{F}\rightarrow\mathcal{D}$ where the functor $\sigma:\overline{F}\to\mathcal{C}$ is Faithful Functor and strictly surjective on both objects and morphisms (and thus Fully Faithful and ESO)

If we interpret this into dependent type theory, we want to think of the functor $\tau:\overline{F}\to\mathcal{D}$ as a Bundle rather than a functor; this leads to the following unfolded definition, where an anafunctor consists of:

• A type of specifications $F:\mathcal{D}\to\mathrm{Type}$
• A Surjective Function $\sigma:F_{d}\to\mathcal{C}$
• For every $d_{1},d_{2}:\mathcal{D}$, $x:F_{d_{1}}$, $y:F_{d_{2}}$, and morphism $f:\mathcal{C}(\sigma(x),\sigma(y))$, a morphism $F(f):\mathcal{D}(d_{1},d_{2})$
• For every $d:\mathcal{D}$ and $x:F_{d}$, $F(\mathrm{id}_{\sigma(x)})=\mathrm{id}_{d}$
• For every $d_{1},d_{2},d_{3}:\mathcal{D}$, $x:F_{d_{1}}$, $y:F_{d_{2}}$, $z:F_{d_{3}}$, $f:\mathcal{C}(\sigma(y),\sigma(z))$, and $g:\mathcal{C}(\sigma(x),\sigma(y))$, we have that $F(f\circ g)=F(f)\circ F(g)$.

Homotopy theoretic interpretation

Recall that the Trivial Fibrations in the Canonical model structure on Cat are surjective-on-objects equivalences. If we rexamine our definition in terms of spans, we can note that the left leg $\sigma:\overline{F}\to\mathcal{C}$ is such a functor; this means that an anafunctor is a presentation of the data of a functor that "remembers" it's trivial fibration factorisation.