Explicit construction of a initial object in a topos

Let $\mathcal E$ be a topos as in Mac Lane and Moerdijk.
A initial object in $\mathcal E$ can be obtained as the domain of the equalizer of the morphisms $P!,\epsilon P1:P1\to P^31$, where $1$ is a terminal object, $!:P^21\to 1$ is the unique morphism and $\epsilon$ is the counit of the adjunction $P^{op}\dashv P$.

Let $A$ be a object in $\mathcal E$.
How to construct explicity the unique morphism $0\to A$?

Solutions Collecting From Web of "Explicit construction of a initial object in a topos"

The method used by Mac Lane and Moerdijk (after Paré) is very elegant and efficient, but also rather abstract. Zhen Lin has given a nice response within this abstract framework.

If the method seems too abstract (i.e., hard to visualize or intuit), there are alternatives. One is to develop some internal logic from scratch, defining operators $\Rightarrow$ and $\forall$ on subobject lattices and then defining an internal intersection operator $P P A \to P A$ by writing down a formula for the intersection in terms of logical operators. Then define the initial object as the subobject of $1$ that is classified by the composite

$$1 \stackrel{t_{P 1}}{\to} P P 1 \stackrel{\bigcap}{\to} P 1$$

whose meaning is “take the intersection of the family of all subobjects of $1$”. This at least produces the minimal subobject $0$ of $1$. Now let $A$ be any object, and take the pullback of the singleton map $\sigma_A: A \to P A$ along the composite map $0 \to 1 \stackrel{t_A}{\to} P A$. Call the pullback $P$; then the map $P \to 0$ is a pullback of the monic $\sigma_A$, hence itself monic, hence an iso because $0$ is the minimal subobject of $1$ by construction. This means we have a map $0 \cong P \to A$ (where the map $P \to A$ is the other pullback projection).

This point of view can be found in some notes I wrote up, here.

The (co)monadicity result implies that, for all objects $X$ in $\mathcal{E}$, $\epsilon_X : X \to P^2 X$ is the equaliser of $\epsilon_{P^2 X}, P^2 \epsilon_X : P^2 X \to P^4 X$. Thus, to construct a morphism $0 \to X$, it is enough to find a morphism $f : 0 \to P^2 X$ such that $\epsilon_{P^2 X} \circ f = P^2 \epsilon_X \circ f$. Consider $P ! : P 1 \to P^2 X$ and $P^3 ! : P^3 1 \to P^4 X$. By naturality, $P^3_! \circ \epsilon_{P 1} = \epsilon_{P^2 X} \circ P !$, and by functoriality, $P^3 ! \circ P ! = P^2 \epsilon_X \circ P !$. Thus, we may take $f : 0 \to P^2 X$ to be the composite $0 \to P 1 \stackrel{P !}{\to} P^2 X$, and this induces the required morphism $0 \to X$.