Question

This may be a little tangential to the original question, but it avoids Choice, and 'works with all choices at once'. In Makkai's theory of anafunctors, one recognizes that 'the' functor $C^J \to C$ giving a limit of a (small) diagram $J \to C$ is only really defined via universal properties, and so requires Choice. However, there is a unique anafunctor $C^J$ ⇸ $C$ - which is a span $C^J \leftarrow D \to C$ where the left-pointing leg is fully faithful and surjective on objects - expressing the limit. The category $D$ is defined to consist of limit cones and maps between them. The functor to $C^J$ forgets the vertex of the cone, and the functor to $C$ forgets the diagram and keeps the vertex. The universal properties take care of functoriality, and if one can choose a limit for each diagram, or there are canonical constructions of limits, then this can be converted into an ordinary functor. The cost of working with anafunctors rather than functors is that one gets a bona fide bicategory of categories, rather than a 2-category, but otherwise the whole theory of categories goes through.