ETCS set theory: Are empty sets isomorphic?

Question

Just a quick question about ETCS: Are any two empty sets isomorphic? Here, a set $X$ is empty if there exists no $x \in X$, i.e. no functions $x: 1 \to X$.

The reason I'm asking is that I need this to show that empty sets are initial sets.

Thank you!

Answer 1

In the case of the theory of sets as a well-pointed topos, if an object is empty it will be initial. Take $i:0\to A$ and $id_A:A\to A$. Assuming $A$ non-initial, $0$ will not be isomorphic with $A$, so $\chi_i:A\to\Omega\neq\chi_{id_A}:A\to\Omega$. By well-pointedness, there must be a point $x:1\to A$ that distingushes them. Hence from $\neg(A\cong 0)$ we have derived that $A$ must have a point.

EDIT: Forgot an important extra piece of information: Initial objects must be empty in a Cartesian closed category, on pain of triviality. So all non-initial objects are non-empty, and all initial objects (by assumption in most topoi) are empty.

Answer 2

Let $\mathcal{S}$ be an externally two-valued elementary topos with the axiom of finite choice, i.e. there are only two subobjects of $1$ in $\mathcal{S}$ (up to isomorphism) and any epimorphism with codomain $1$ is a split epimorphism. If $X$ is an object in $\mathcal{S}$ such that there do not exist any morphism $1 \to X$, then $X$ is an initial object in $\mathcal{S}$. Indeed, let $U \rightarrowtail 1$ be the image of the unique morphism $X \to 1$. If $U$ is a terminal object then the unique morphism $X \to 1$ is an epimorphism, in which case the axiom of finite choice implies it has a section, i.e. there exists a morphism $1 \to X$. Thus $U$ is not a terminal object – so it must be an initial object, by two-valuedness. But initial objects in cartesian closed categories are strict, so $X \to U$ must be an isomorphism, and so $X$ must itself be an initial object.

Note that $\mathcal{S}$ need not be well-pointed for the above proof to work: for example, $\mathcal{S}$ could be the topos of simplicial sets. Conversely, any non-degenerate elementary topos with the property that "empty objects are initial" must be externally two-valued and have the axiom of finite choice.