It's a [ZFC theorem of Freyd](https://ncatlab.org/nlab/show/complete+small+category), any small complete category is a preorder. Freyd's theorem continues to hold [in any Grothendieck topos](https://mathoverflow.net/questions/43433/small-complete-categories-in-a-grothendieck-topos "Small complete categories in a Grothendieck topos"). But Hyland showed it fails [in some elementary toposes](https://ncatlab.org/nlab/show/complete+small+category#in_more_general_toposes_and_constructive_mathematics).


I don't actually know, but I suspect that Hyland's topos examples don't readily translate into models of ZF — toposes don't play well with replacement. So


**Question:** Does Freyd's theorem hold in ZF?


That is, in ZF is every small complete category a preorder?



Can there be a small complete category in ZF?
Yes, Freyd's theorem holds in ZF. The theorem relies on excluded middle, choice does not play a role. Just to be sure, let's work with excluded middle but without choice.


**Theorem:** *A small-complete small category is a preorder.*


*Proof.* Let $C$ be a small-complete small category, with $C\_0$ the set of objects and $C\_1$ the set of morphisms. Consider any $x, y \in C\_0$. We need to show that the set of morphisms $C(x,y)$ contains at most one element. For this purpose, suppose $r\_0 : x \to y$ and $r\_1 : x \to y$. By excluded middle it suffices to show that $r\_0 \neq r\_1$ leads to a contradiction. So assume $r\_0 \neq r\_1$, and define $z = \prod\_{C\_1} y$, the $C\_1$-fold product of $y$'s. Note that a morphism $h : x \to z$ is given as a $C\_1$-indexed family $h = \langle h\_f \rangle\_{f \in C\_1}$ of morphisms $h\_f : x \to y$.


Define the map $i : \{0,1\}^{C\_1} \to C\_1$ by
$$i(c) = \langle r\_{c(f)}\rangle\_{f \in C\_1} : x \to z.$$
we claim that $i$ is injective, which is impossible because it would give us a surjection $C\_1 \to \{0,1\}^{C\_1}$ by excluded middle, contradicting Cantor's theorem (which is constructive). To see that $i$ is injective, suppose $i(c) = i(d)$. Then $r\_{c(f)} = r\_{d(f)}$ for all $f \in C\_1$, but since $r\_0 \neq r\_1$ it follows that $c(f) = d(f)$ for all $f \in C\_1$ (no excluded middle here because equality on $\{0,1\}$ is decidable), hence $c = d$. $\Box$


In the above proof there two applications of excluded middle: concluding $r\_0 = r\_1$ from $\lnot\lnot (r\_0 = r\_1)$, and obtaining a surjection $C\_1 \to \{0,1\}^{C\_1}$ from an injection $\{0,1\}^{C\_1} \to C\_1$. As far as I can tell, both are necessary. And we never used choice.


