anafunctor category

Given categories CC and DD, the anafunctor category D CD^C has anafunctors F:CDF: C \to D as objects and ananatural transformations between these as morphisms.

This is the appropriate notion of functor category to use in the absence of the axiom of choice (including many internal situations).

Functor categories serve as the hom-categories in the anabicategory Cat.