nLab
complete small category

Definition

A complete small category (or small complete category) is a category which is both small (has only a set of objects and morphisms) and complete (has a limit of every small diagram).

(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.)

In classical logic

In the presence of classical logic, complete small categories reduce to complete lattices by the following theorem of Freyd.

Theorem

If (in some universe $U$) a small category $D$ has products of families of objects whose size is at least that of its set of morphisms, then $D$ is a preorder. In particular, any complete small category is a preorder.

Proof

Let $x$, $y$ be any two objects, and suppose (contrary to $D$ being a preorder) that there are at least two different morphisms $x\underset{s}{\overset{r}{\rightrightarrows }}y$. Then the set of morphisms

$$x\to \prod _{f\in \mathrm{Mor}(D)}y$$x \to \prod_{f \in Mor(D)} y

has cardinality at least $2^{\mid \mathrm{Mor}(D)\mid }>\mid \mathrm{Mor}(D)\mid$, which is a contradiction.

In Grothendieck toposes

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 $\mathrm{Set}$. A brief description of the argument can be found in the answer to this question.

In more general toposes and constructive mathematics

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 $\mathrm{Set}$ or in a Grothendieck topos must be a preorder.