I am not able to formalize my question, so instead let me begin with an example:
Lemma: Given a functor $F: \mathcal C \times \mathcal D \to \mathcal E$, if $\mathcal E$ is complete, then for any morphism $c : C \to C'$ in $\mathcal C$ we have a map $\lim_{D\in \mathcal D} F(c,D) : \lim_{D\in \mathcal D} F(C,D) \to \lim_{D\in \mathcal D} F(C',D)$ that satifies that a certain square commute (not relevant but you can guess it).
Now, consider the following statement and it's proof:
Proposition: Let $F: \mathcal C \times \mathcal D \to \mathcal{Set}$ be a functor and let $c : C \to C'$ in $\mathcal C$. Take the limits to be the usual equalizer of products. Then $\lim_{D\in \mathcal D} F(c,D)$ is defined by $$\lim_{D\in \mathcal D} F(c,D)((x_D)_{D\in \mathcal D}) = (F(c,1_D)x_D)_{D\in \mathcal D}$$
Proof: By the lemma, we know that a function $\lim_{D\in \mathcal D} F(c,D) : \lim_{D\in \mathcal D} F(C,D) \to \lim_{D\in \mathcal D} F(C',D)$ exists, but with the given data in the proposition, the only way to define such a function is the way we defined it; therefore, that must be the required function.
Note that we get "for free" that the required square commutes.
This proof seems to say the least, weird. However at the same time it seems right to me. Obviously, such reasoning can't apply for everything, because of nonconstructive proofs. However, it is not obvious to me that constructivity of a Lemma is enough to allow for such proofs.
My questions are then:
- What are sufficient conditions for such reasoning be valid?
- What, if any, is the precise formulation of the meta-lemma that's being invoked when doing such reasoning?
This comes from practical considerations, as this situation arises many times when working in category theory, specially in $\mathcal{Set}$. Some examples: RAPL, interchange of limits or colimits, the representation of functors as colimits of representable functors, etc.
My own attempt to 1. and 2. is:
Conjecture: Fix a formal system (e.g. ZF). Given a constructive lemma of the form "Given some data $D$ satisfying conditions $\psi(D)$, then there is a unique morphism $f:A_D \to B_D$ that satisfies $\varphi(f)$", if I have some constructively-obtained data $D'$ with $\psi(D')$, and furthermore given this data, there's only one function $f':A_{D'} \to B_{D'}$ that can be constructively defined, then $\varphi(f')$.