Classically, if a (locally small) category $C$ has all limits of shape $K$ (for some small diagram $K$), then its free co-completion also has $K$-shapped limits.

But all proof I know of that result relies on the axiom of choice at some point (for $K$ infinite). Is the result true constructively? Or can we build a counter-example (or show that it implies something non-constructive).

I'm mostly interested in the case where $C$ has all limits, and I want to show that the free cocompletion has arbitrary product.

For some details: When $C$ is a small category, it's free cocompletion is the category $P(C)$ of presheaves of sets on $C$, which obviously has all limits. The problem arise when $C$ is just locally small. In this case, a free co-completion still exists, but it is now the category $P^s(C)$ of "small preshaves" on $C$, which is the full subcategory of $P(C)$ of objects which a small colimits of representables (And $P^s(C)$ is then again a locally small category). Alternatively, it can be defined as: $$ P^s(C) = \operatorname*{colim}_{D \subset C, D \text{ small}} P(D)$$

where the colimits is over all small full subcategory $D \subset C$.

And it is no longer clear that $P^s(C)$ has all limits: It is equivalent to the question of whether small limits of small presheaves are small presheaves. A classical result assert that if (for a given shape of limits) the limits of representable are small preaves (in particular if they are representable) then limits (of the same shape) of general small presheaves are small again. But it is unclear to me that a similar result can be obtained constructively (for e.g. under the assumption that $C$ has all limits).

Classically, if a locally small category $C$ has all limits of shape $K$ (for some small diagram $K$), then its free co-completion also has $K$-shapped limits.

But all proof I know of that result relies on the axiom of choice at some point (for $K$ infinite). Is the result true constructively? Or can we build a counter-example (or show that it implies something non-constructive).

I'm mostly interested in the case where $C$ has all limits, and I want to show that the free cocompletion has arbitrary product.

For some details: When $C$ is a small category, it's free cocompletion is the category $P(C)$ of presheaves of sets on $C$, which obviously has all limits. The problem arise when $C$ is just locally small. In this case, a free co-completion still exists, but it is now the category $P^s(C)$ of "small preshaves" on $C$, which is the full subcategory of $P(C)$ of objects which a small colimits of representables (And $P^s(C)$ is then again a locally small category). Alternatively, it can be defined as: $$ P^s(C) = \operatorname*{colim}_{D \subset C, D \text{ small}} P(D)$$

where the colimits is over all small full subcategory $D \subset C$.

And it is no longer clear that $P^s(C)$ has all limits: It is equivalent to the question of whether small limits of small presheaves are small presheaves. A classical result assert that if (for a given shape of limits) the limits of representable are small preaves (in particular if they are representable) then limits (of the same shape) of general small presheaves are small again. But it is unclear to me that a similar result can be obtained constructively (for e.g. under the assumption that $C$ has all limits).

Classically, if a category $C$ has all limits of shape $K$ (for some small diagram $K$), then its free co-completion also has $K$-shapped limits. But all proof I know of that result relies on the axiom of choice at some point (for $K$ infinite). Is the result true constructively? Or can we build a counter-example (or show that it implies something non-constructive).

I'm mostly interested in the case where $C$ has all limits, and I want to show that the free cocompletion has arbitrary product.

For some details: When $C$ is a small category, it's free cocompletion is the category $P(C)$ of presheaves of sets on $C$, which obviously has all limits. The problem arise when $C$ is not a small category. IN this case, a free co-completion still exists, but it is now the category $P^s(C)$ of "small preshaves" on $C$, which is the full subcategory of $P(C)$ of objects which a small colimits of representables. Alternatively, it can be defined as: $$ P^s(C) = \operatorname*{colim}_{D \subset C, D \text{ small}} P(D)$$

where the colimits is over all small full subcategory $D \subset C$.

And it is no longer clear that $P^s(C)$ has all limits: It is equivalent to the question of whether small limits of small presheaves are small presheaves. A classical result assert that if (for a given shape of limits) the limits of representable are small preaves (in particular if they are representable) then limits (of the same shape) of general small presheaves are small again. But it is unclear to me that a similar result can be obtained constructively (for e.g. under the assumption that $C$ has all limits).

Classically, if a (locally small) category $C$ has all limits of shape $K$ (for some small diagram $K$), then its free co-completion also has $K$-shapped limits. 

But all proof I know of that result relies on the axiom of choice at some point (for $K$ infinite). Is the result true constructively? Or can we build a counter-example (or show that it implies something non-constructive).

I'm mostly interested in the case where $C$ has all limits, and I want to show that the free cocompletion has arbitrary product.

For some details: When $C$ is a small category, it's free cocompletion is the category $P(C)$ of presheaves of sets on $C$, which obviously has all limits. The problem arise when $C$ is just locally small. In this case, a free co-completion still exists, but it is now the category $P^s(C)$ of "small preshaves" on $C$, which is the full subcategory of $P(C)$ of objects which a small colimits of representables (And $P^s(C)$ is then again a locally small category). Alternatively, it can be defined as: $$ P^s(C) = \operatorname*{colim}_{D \subset C, D \text{ small}} P(D)$$

where the colimits is over all small full subcategory $D \subset C$.

And it is no longer clear that $P^s(C)$ has all limits: It is equivalent to the question of whether small limits of small presheaves are small presheaves. A classical result assert that if (for a given shape of limits) the limits of representable are small preaves (in particular if they are representable) then limits (of the same shape) of general small presheaves are small again. But it is unclear to me that a similar result can be obtained constructively (for e.g. under the assumption that $C$ has all limits).