Can ETCC/ETCS talk about 'size issues'?

In material set theories (like ZFC), one can prove that there is no set of all sets. Can one prove a similar statement in ETCS? This exact statement "there is no set x such that y in x for every set y" is not expressible in ETCS because ETCS is a structural set theory. But however is there a way to nevertheless talk about size issues in ETCS?

Also, in ETCC, which axiomatizes the category of categories, can one there prove/formulate a statement like "There is no category that contains every category"?

• One should mention algebraic set theory as well, which is an axiomatisation of a category of classes. – David Roberts Mar 13 '17 at 3:51
• Here is a related statement: There is no object $X$ (of our topos of sets) such that every object $Y$ admits a monomorphism $Y \to X$. – HeinrichD Mar 17 '17 at 13:34

We can talk about a family of sets $Y_x$ parameterized by the elements $x \in X$ of another set using a bundle of sets, namely a map

$$Y = \bigsqcup_{x \in X} Y_x \mapsto X$$

whose fibers are the family of interest. This is, for example, how ETCS talks about the axiom of choice. So we can phrase the nonexistence of a "bundle of all sets" as the following claim.

Claim: There is no map $f : Y \to X$ such that, for every set $S$, there exists $x \in X$ such that $S \cong f^{-1}(x)$.

(Note that $x \in X$ is the same as saying $x : 1 \to X$ and $f^{-1}(x)$ is the pullback of the diagram $1 \xrightarrow{x} X \xleftarrow{f} Y$; this really is an entirely categorical statement.)

What I want to say from here is that we should pick $S = 2^Y$ and then appeal to Cantor's theorem, or more categorically the Lawvere fixed point theorem. But what we need is a surjection $Y \to 2^Y$ and what we get is an injection $2^Y \to Y$, and I'm not sure how much of ETCS is necessary to make everything work out.

• In any topos, the subobject classifier is internally injective, so that any injection $A\rightarrowtail B$ yields a surjection $\Omega^B \twoheadrightarrow\Omega^A$. Thus, an injection $\Omega^Y \rightarrowtail Y$ gives a surjection $\Omega^Y \to \Omega^{\Omega^Y}$, allowing us to apply Cantor's theorem. – Mike Shulman Mar 13 '17 at 12:12