ETCS set theory: Are empty sets isomorphic?

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!

• Any two initial objects are isomorphic, in a unique way. So it suffices to show that empty sets are initial. – Zhen Lin Nov 14 '13 at 22:35
• is there more than one empty set? – magma Nov 14 '13 at 22:41
• @ZhenLin: Yes, but the problem lies in showing that empty sets are initial. If $X$ is empty and $Y$ is any set, then how does one cook up a function $X \to Y$ when $Y$ is empty? – Ulrik Nov 14 '13 at 22:48
• @magma: In ZFC there is only one empty set by extensionality, but in ETCS I don't think there's any problem in having several empty sets. – Ulrik Nov 14 '13 at 22:50
• That statement presupposes a notion of $\mathbf{Set}$, which is precisely what ETCS is axiomatising! – Zhen Lin Nov 16 '13 at 16:50

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