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](https://mathoverflow.net/a/336610/475802) 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](https://nforum.ncatlab.org/discussion/2449/complete-small-category/?Focus=25906#Comment_25906)), 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.


1. 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*](https://arxiv.org/abs/0810.1279), §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](https://mathoverflow.net/questions/43433/small-complete-categories-in-a-grothendieck-topos?noredirect=1&lq=1)) doesn't help either, since they reduce to internal categories in $\mathbf{Sets}$: small + strict.
2. 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.



Small complete categories in HoTT+LEM
Here is an alternative proof based on Russell's paradox rather than cardinality that doesn't require sets cover, although I do need to assume that hom sets are 0 truncated. The rough outline is to modify Gylterud's definition of the cumulative hierarchy by limiting it to sets that can be constructed from $\mathcal{C}$ to make it a small type, and then follow the usual proof of Russell's paradox.


The first step is the following lemma.


**Lemma** There is a small type $X : \mathcal{U}$ together with an embedding $\iota : X \hookrightarrow \mathcal{U}$ such that every type that can be expressed as a set quotient of a subtype of a type of the form $\mathcal{C}(a, b)$ for $a, b : \mathcal{C}\_0$, is equivalent to one in the image of $\iota$.


**Proof** For each $a, b : \mathcal{C}\_0$ we can express every subobject $Z \hookrightarrow \mathcal{C}(a, b)$ of $\mathcal{C}(a, b)$ as $\sum\_{f : \mathcal{C}(a, b)} \chi(f) = 1$ for some map $\chi: \mathcal{C}(a, b) \to 2$. Furthermore, every set quotient of $Z$ is the quotient of some equivalence relation $R : Z \times Z \to 2$. This gives a type $Y$ together with a map $Y \to \mathcal{U}$ whose image contains every set quotient of every subtype of $\mathcal{C}(a, b)$ for every $a, b : \mathcal{C}\_0$. By type theoretic replacement (Theorem 4.6 in Rijke, [*The join construction*](https://arxiv.org/abs/1701.07538)), we can take the image of this map to be small type, which is the required $X$.$\quad \square$


Next we construct a modified version of the Aczel cumulative hierarchy $M$ as the $W$-type with constructors $X$, and the arity of $x : X$ is just $\iota(x)$. Note that since $X$ is a small type, and all the arities are small, so is $M$, unlike the usual Aczel hierarchy. We then construct a retract of $M$ corresponding to the construction of the HIT cumulative hierarchy in Gylteud, [*From multisets to sets in homotopy type theory*](https://doi.org/10.1017/jsl.2017.84). Namely an element of $M$ of the form $\sup(x, \alpha)$ for $x : X$ and $\alpha : \iota(x) \to M$ is a *hereditary embedding* if $\alpha$ is an embedding and $\alpha(y)$ is a hereditary embedding for all $y : \iota(x)$. Write $V$ for the subtype of $M$ consisting of hereditary embeddings. Since $V$ is a subtype of $M$, it is also small. Following the same argument that Gylterud used for the cumulative hierarchy (section 5 of paper above), $V$ is necessarily 0-truncated. We define membership $\in$ the same as Gylterud does.


Now suppose that we are given $f \neq g : \mathcal{C}(a, b)$. Define $c$ to be the product $\prod\_V b$. We have injections $V \hookrightarrow 2^V \hookrightarrow \mathcal{C}(a, c)$. Since $V$ and $\mathcal{C}(a, c)$ are both sets, this gives us a surjection $s : \mathcal{C}(a, c) \twoheadrightarrow V$. We define a subtype $Z$ of $V$ as $Z := \sum\_{z : V} z \notin z$. Pulling back along $s$ gives us a subtype $Z'$ of $\mathcal{C}(a, c)$ together with a surjection $Z' \twoheadrightarrow Z$. Since $Z'$ and $Z$ are both sets, $Z$ must be a set quotient of $Z'$. Hence $Z$ is equivalent to $\iota(x)$ for some $x$. Hence we have $z\_0 : V$ such that for all $z \in z\_0 \;\simeq\; z \notin z$ for all $z : V$, which gives a contradiction by Russell's paradox.


