Freyd's theorem in classical category theory says that any small category $\mathcal{C}$ admitting products indexed by the set $\mathcal{C}_1$ of all its arrows is a preorder. I'm interested in whether this is also true for for precategories/univalent categories à lá HoTT Book (§II.9), provided we assume LEM.

I'll refer to the notation from Andrej Bauer's very clear presentation of the proof. In particular, $f, g : a \to b$ are morphisms with $f \ne g$, and $z$ is the large product $\prod_{\mathrm{Arr}(\mathcal{C})} b$.

In HoTT (and, potentially, others where equality of objects is problematic), there is no general way of embedding $\mathcal{C}(a,b) \to \mathcal{C}_1$, so while it is possible to construct the map the map $i : \{0,1\}^{\mathcal{C}_1} \to \mathcal{C}_1$ from the linked answer, showing this map is an embedding is impossible. If we instead consider the assignment $c \mapsto \langle r_{c(i)}\rangle_i $ from the linked answer to define a function $i : \{0,1\}^{\mathcal{C}_1} \to \mathcal{C}(a, z)$ we *do* get an embedding.

An example of $\mathcal{C}, a, b$ for which the evident map $\mathcal{C}(a,b) \to \mathcal{C}_1$ fails to be an embedding is obtained by taking $\mathcal{C} = \mathbf{Sets}$, and $a, b = \{0,1\}$. Then we have $(a, b, \mathrm{id}) = (a, b, \mathrm{not})$ in the groupoid of arrows, but the identity function is not the negation function. Of course, the category of sets fails to be large-complete for other reasons, but the point stands: we can not embed a $\mathrm{Hom}$-set into the space of all arrows unless we know *a priori* that $\mathcal{C}_1$ is a set.

If $\mathcal{C}_0$ admits a surjection $c : X \twoheadrightarrow \mathcal{C}_0$ from a set, then we can consider a modified definition of $\mathcal{C}_1$ which allows the traditional proof to be repaired: Rather than the sum $\sum_{(a,b) : \mathcal{C}_0 \times \mathcal{C}_0} \mathcal{C}(a,b)$, we define $\mathcal{C}_1'$ by summing over $X \times X$ instead, and use *this* type to construct $i$. Since we're aiming for a contradiction, we can assume we've been given $a', z' : X$ with identifications $p_a : c(a') = a$ (resp. $p_z : c(z') = z$); The composite

$$ \{0,1\}^{\mathcal{C}'_1} \hookrightarrow \mathcal{C}(a,z) \simeq C(c(a'), c(z')) \hookrightarrow\mathcal{C}'_1 $$

is verified to be an embedding. Replacing $\mathcal{C}_0$ by $X$ comes in at the last step, where we're given $(a, b, i(f)) = (a, b, i(g)) : \mathcal{C}_1'$ and want to conclude $i(f) = i(g)$ (thus $f = g$). Since $(a, b)$ now inhabits the set $X \times X$, this is allowed.

This modified proof establishes that Freyd's theorem holds in e.g. the simplicial sets model of HoTT, which satisfies excluded middle *and* sets cover. However, I'm a bit surprised that we had to assume sets cover! It's true that sometimes "small" means "small, strict" (e.g.: "the category of small categories is monadic over that of graphs"), but the statement of Freyd's theorem doesn't, at a glance, mention anything that disrespects equivalence: completeness, being a preorder, and the arrow category are all invariant.

Is Freyd's theorem

*really*one of the cases where small means small*and strict*, or is there an alternative proof that does not assume $\mathcal{C}(a,z) \hookrightarrow \mathcal{C}_1$? Other proofs of Freyd's theorem in the literature (e.g. in Shulman's*Set theory for category theory*, §2.1; Freyd's original in*Abelian Categories*, §3.D) are all expressed in a set-theoretic framework, and follow the same strategy as Andrej's. The generalisation to the internal logic of a Grothendieck topos (e.g. here) doesn't help either, since they reduce to internal categories in $\mathbf{Sets}$: small + strict.Assuming that the theorem isn't salvageable, can we have a complete small category that's not a preorder? This would be a very interesting gadget!

I think it can't be any of the usual suspects which become "large-complete" under "impredicative Set", since for any such $\mathcal{C}$ and endofunctor $F : \mathcal{C} \to \mathcal{C}$, the category of $F$-algebras inherits limits from $\mathcal{C}$, and so also has "limits its own size" --- in particular for the identity $\mathrm{Id} : F\mathrm{-Alg} \to F\mathrm{-Alg}$. By Lambek's theorem, this means every endofunctor on $\mathcal{C}$ has a fixed point.