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.
Best Answer
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.