Some choice functions can be specified explicitly, while in other cases no definite choice function is known. An example of the former is a choice function for non-empty subsets of natural numbers, where one can always pick the smallest element. An example of the latter is a choice function for non-empty subsets of real numbers. A common intuition is that these explicit choice functions have uniform definitions (or at least the number of non-uniform cases must be limited). This is reminiscent of natural transformations, which can capture the idea of a morphism defined uniformly with respect to objects in a category.
Is there a way to formalize the uniformity intuition for definite choice functions? Specifically, is there some invariance/coherence condition the "pick the minimum" on the naturals satisfies that no choice function on the reals could satisfy?
It seems like by "explicit" choice function you mean a choice function that can be defined in $\mathsf {ZF}$, without needing the Axiom of Choice.