In category theory, does a definition via a universal property induce a functor? In category theory one frequently defines concepts via universal properties. Examples are

*

*(co)equalizers of pairs of morphisms having the same domain and codomain


*(co)kernels of morphisms in categories with zero-objects


*(co)products of families of objects


*limits of inverse systems / colimits of direct systems
Such definitions normally do not produce unique results, things are only determined up to  "canonical" isomorphism.
On the other hand, one often reads that such definitions allow to define functors having the approprioate universal properties. As an example, if $\mathcal C$ is a category with finite products, there should be a functor
$$P : \mathcal C \times  \mathcal C \to \mathcal C$$
such that $P(A,B)$ is "the" product object of $A, B \in  \mathcal C$.  Okay, this $P$ does not really allow to capture the universal property of the product, so perhaps one should better regard $P$ as functor into a category $\mathcal C'$ of certain diagrams in $\mathcal C$ such that $P(A,B)$ has the universal property of the product.
The essential point is this:
Since products are only determined up to isomorphism, we have to make a choice for any pair $(A,B)$. This seems to require a variant of the axiom of choice for classes - which appears to be very dubious.
So what can be done to settle the choice problem? Do we need further assumptions to make definitions via universal properties functorial?
 A: After pondering about Zhen Lin's comment, it seems to me that this only a theoretical problem.
If we only know that $\mathcal C$ has "things" described via a universal property, then we get indeed a choice problem. Since the objects of $\mathcal C$ in general form a proper class, we would need a version of the axiom of choice for classes. My knowledge about set theory is limited, but I have never seen such a general  choice axiom and can't judge which problems  it could cause.
The general pattern of a universal property is this: We are given a diagram $\Delta$ in $\mathcal C$ consisting of a family of objects $(X_i)_{i \in I}$ and a family of morphims between these $X_i$. Then we consider diagram extensions $\Delta^*$ obtained from $\Delta$ by adding a single object $X(\Delta^*)$ and morphisms between $X(\Delta^*)$ and the $X_i$ such that some characteristic condition $\mathfrak P$ is satisfied. We consider two types of diagram extensions: Sink extensions in which all added morphisms have codomain $X(\Delta^*)$, i.e. have the form $f_i^{\Delta^*} : X_i \to X(\Delta^*)$, and source extensions in which  all added morphisms have domain $X(\Delta^*)$, i.e. have the form $f_i^{\Delta^*} : X(\Delta^*) \to X_i$.
Let us focus on sink extensions; everything can of course be formulated "dually" for source extensions.
A morphism from a sink extension $\Delta_1^*$ to a sink extension $\Delta_2^*$ is a morphism $\phi: X(\Delta_1^*) \to X(\Delta_2^*)$ such that $f_i^{\Delta_2^*} \circ \phi = f_i^{\Delta_1^*}$ for all $i \in I$.
A sink extension $\Delta_u^*$ is called a universal sink extension of characteristic $\mathfrak P$ if for each source extension $\Delta^*$ there exists a unique morphism $\phi : X(\Delta^*) \to X(\Delta_u^*)$.
Equalizers, kernels, products and limits are examples of universal sink extensions; coequalizers, cokernels, coproducts and colimits are examples of universal source extensions. So perhaps we should call a source extension a cosink extension.
How do we know that a diagram $\Delta$ in a category $\mathcal C$ has a  universal sink or source extension?
Certainly we have to give a proof, and this requires an explicit construction assigning to $\Delta$ an object $X_u(\Delta)$ and morphisms between $X_u(\Delta)$ and the $X_i$. Such a constructive existence proof usually will not involve any choices; it works like a (deterministic) algorithm.
In other words, we get a function assigning to an input consisting of a diagram $\Delta$ an output consisting of a specific universal extension $\Delta^*_u$.
Therefore, if we have some category $\mathcal C^*$ of diagrams in $\mathcal C$ with universal universal sink or source extensions of characteristic $\mathfrak P$, we get a functor
$$\mathfrak P^* : \mathcal C^* \to \mathcal C^s$$
where $\mathcal C^s$ denotes the category of sink or source diagrams in $\mathcal C$.
