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.