An elementary topos is a category that:
- has finite limits
- is cartesian closed
- has a subobject classifier
and one can show (with quite a bit of effort) that it has finite colimits.
Is there, starting from the axioms, a quick and easy way to see that it has an initial
object? What part of the axioms are really needed to prove this?
Motivation: Occasionally people discuss whether there should be a map $\emptyset \to \emptyset$. If there is not, then we need to stop talking about the empty "set" and $\mathsf{Set}$ fails to have an initial object, hence fails to be a topos. I want to see what part of the axioms above are actually violated by that, i.e. how $\mathsf{Set}$ fails to be a topos.
Best Answer
I believe that you can construct the initial object elementarily in the following steps, with no knowledge about monadicity needed.
Recall that we can define for any object $A$ the universal quantification operator $\forall_A : \Omega^A \to \Omega$ as the classifying morphism of the subobject $1 \to \Omega^A$ with transpose given by $1 \times A \to 1 \xrightarrow{t} \Omega$, where $t$ is the universal monomorphism. (In $\mathrm{Set}$, for a family $f : A \to \Omega$ of truth values, $\forall_A(f)$ is the truth value of $\forall x \in A{:}\ f(x)$.)
In particular, we can construct the global element of $\Omega$ denoting falsity as the composition $1 \to \Omega^\Omega \xrightarrow{\forall_\Omega} \Omega$, where $1 \to \Omega^\Omega$ is the transpose of $\Omega \xrightarrow{\mathrm{id}} \Omega$. (In $\mathrm{Set}$, this global element is the truth value of $\forall \varphi \in \Omega{:}\ \varphi$, i.e. $\bot$.)
We then obtain the initial object as the subobject classified by this morphism.
To verify that the constructed object is indeed the initial object, you probably need to know the universal property of $\forall_A$. It is given, with full proof, in Theorem 13.3 of Thomas Streicher's beautiful notes on category theory and categorical logic.