It is a classical theorem of Freyd that if a small category is complete (has all small limits—in fact, having small products suffices), then it is a preorder (has at most one morphism between any two objects). The proof of this theorem (which can be found here or in CWM) is non-constructive, i.e. it uses the Law of Excluded Middle. Therefore, it can potentially fail in the internal logic of an elementary topos. And in fact, it *does* fail in the effective topos, and more generally in realizability topoi, where there do exist small complete categories that are not preorders.

However, I have heard it said that Freyd's theorem cannot fail in a *Grothendieck* topos; i.e. that a small complete category in a Grothendieck topos must still be a preorder—despite the fact that the internal logic is still in general intuitionistic, so that Freyd's proof cannot work. Can someone explain why this is, or (even better) give a reference containing a proof?