The Stacks project

I think this proof is a little tricky whenever $S^{-1}\mathcal{C}$ is not locally small (for non-small $\mathcal{C}$) because of the size issues I discuss here. Nevertheless, one can avoid these size issues and show existence of finite products via this argument.

All categories are small unless mentioned otherwise... discussed elsewhere...

@#9219 I am aware about the SP convention that everything is a small category (unless otherwise stated). My point is that inside the SP itself there may be an application of this result to some non-small category, like, say, the derived category of some non-small abelian category (like $R$-modules or some category of modules over a scheme). It is not far-fetched that something like this might already appear (although I don't know any instance throughout the SP now).

That's not a comment on this lemma however, so I am going to leave this lemma as is.

After we know $Q$ is additive, I think one has a direct proof by Homology, Lemma 12.3.7.