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.

  • 1
    $\begingroup$ You do know there are small-cmplete non-preorders in realizability toposes? $\endgroup$ Jan 15 at 9:47

2 Answers 2


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.

  • 1
    $\begingroup$ This is worth writing up someplace that isn't just an MO answer. (Also, to fill in the details, and to see whether there is a simplification that circumvents $V$.) $\endgroup$ Jan 15 at 9:36
  • $\begingroup$ By the way, which bits here use $2$ as a subjobject classifier (and could use a general subobject classifier $\Omega$ instead), and which bits use excluded middle spefifically? The lemma just uses $\Omega$, right? Excluded middle only appears at the end to get the surjection $s$ from the injection. $\endgroup$ Jan 15 at 9:45
  • $\begingroup$ I was a bit lazy with identifying 2 with the subobject classifier. Yes, it can mostly be replaced with $\Omega$. As Amélia pointed out in the mastodon discussion, the 2 in $2^V$ really is 2 and not $\Omega$. Because of this LEM is necessary to get the map $V \to 2^V$ (because it requires that singletons are decidable subsets). It's also used to get the inverse $s$ to the injection, as you say. $\endgroup$
    – aws
    Jan 15 at 13:57
  • $\begingroup$ After writing the answer I thought a bit more about how it generalises. It would be something like "there is no small family of small sets $Y \to \mathbf{hSet}$ such that every small set is a subquotient of one in the family." This is enough to show the result and follows from Russell's paradox. I'll be too busy the next couple of weeks at least, but yes it probably should be written up properly. $\endgroup$
    – aws
    Jan 15 at 14:04
  • 1
    $\begingroup$ It's quite possible that there's a simpler proof that doesn't use $V$, but I would consider it a different proof to this one. The way this one works needs some way to turn a collection of sets into a set. This seems to need some kind of inductive construction with the cumulative hierarchy the simplest I know about. $\endgroup$
    – aws
    Jan 15 at 14:04

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.