Small complete categories in HoTT+LEM

Question

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.

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, §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.

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.

Answer 1

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

Answer 2

Let's try to fix the "other side" instead: can we modify the proof to give an embedding $2^{C(a,z)} \hookrightarrow C(a,z)$? The embedding $2^{C_1} \hookrightarrow C(a,z)$ in the original proof follows from the fact that by construction $z \cong \prod_{C_1} b$. Thus, we would get an embedding $2^{C(a,z)} \hookrightarrow C(a,z)$ if instead we had $z \cong \prod_{C(a,z)} b$. This would be circular as a direct definition of $z$, but we can interpret it instead as a fixed-point equation to be solved, and recall that (as noted in the question) any endofunctor of a small complete category has a fixed point. The only wrinkle is that $x \mapsto \prod_{C(a,x)} b$ is a contravariant functor $C^{\rm op}\to C$, but we can easily make it covariant by taking another powerset.

In detail, here's the proof. Let $C$ be a small complete precategory (hom-sets but arbitrary type of objects), and suppose $r_0,r_1 \in C(a,b)$; we will show $r_0=r_1$ by deriving a contradiction from $r_0\neq r_1$. Define $F:C\to C$ by $$F(x) = \prod_{2^{C(a,x)}}b.$$ Then the category of $F$-algebras is also small complete (its limits are created in $C$), hence it has a limit of its identity functor, which is an initial object, and by Lambek's lemma an initial $F$-algebra is an isomorphism. Thus, there is an object $z\in C$ with $z\cong F(z)$.

Now we use this to construct an embedding $i:2^{C(a,z)} \hookrightarrow C(a,z)$. Given $f\in 2^{C(a,z)}$, we construct $i(f) \in C(a,z)$ using the universal property of $z \cong \prod_{2^{C(a,z)}} b$, with component $i(f)_p \in C(a,b)$ associated to any $p\in 2^{C(a,z)}$ defined by $$ i(f)_p = \begin{cases} r_0 &\quad \text{if } p=f \\ r_1 &\quad \text{otherwise}\end{cases} $$ This is injective because if $i(f) = i(g)$, then $i(f)_g = i(g)_g = r_0$, hence $g=f$. We now complete the proof as before: LEM implies any embedding with nonempty domain has a retraction, hence a surjection $C(a,z) \twoheadrightarrow 2^{C(a,z)}$, contradicting Cantor's theorem.