(Note that the phrase “small-complete category” is sometimes used to mean merely a complete category, i.e. one which is “complete relative to small diagrams”. Therefore, “complete small category” is a safer term for our concept.)
If (in some universe ) a small category has products of families of objects whose size is at least that of its set of morphisms, then is a preorder. In particular, any complete small category is a preorder.
Let , be any two objects, and suppose (contrary to being a preorder) that there are at least two different morphisms . Then the set of morphisms
has cardinality at least , which is a contradiction.
The internal logic of a topos is not, in general, classical, so the above proof does not apply when considering internal categories in a topos. However, in a Grothendieck topos, one can show that the conclusion still holds by essentially reducing the question to the analogous one in . A brief description of the argument can be found in the answer to this question.
However, it is possible to have non-preorder complete small categories in non-Grothendieck topoi. In particular, the effective topos, along with most other realizability toposes, does contain such internal categories. These categories have applications to the modeling of impredicative type theory.
It follows that, in constructive mathematics, it is impossible to prove even that every complete small category in or in a Grothendieck topos must be a preorder.