$
\def\aut{\text{Aut}}
\def\hom{\text{Hom}}
\def\id{\text{id}}
\def\true{\mathsf{true}}
\def\xra{\xrightarrow}
$In the SiGaL book, they prove that in an elementary topos, every $k:A\to 0$ is an iso, but to me the argument is very involved and not so elucidating (note that the whole machinery of slice categories is not even contained in the screenshot):
I wonder if there is a more fundamental proof for such an important property? As far as I understand, this property is also key for showing $X\times 0\cong 0$ and hence $P(0)\cong 1$.
First, I tried to show it in a more basic setting with only finite limits and colimits, but I think the property fails here. For a counterexample, consider the the category $C$ with objects $X,0,1$ such that $0$ is initial, $1$ is final, and additional arrows $x^*:X\to 0$ $x_i:X\to X$ for $i\in\mathbf{N}$ satisfying the equalities $x_0=\id_X$, $x_1=0_Xx^*$ and $x_ix_j=x_{i+j}$. I believe to have shown that $C$ has finite limits and colimits. For a cone $F:D\to C$ such that $X$ is not contained in the cone, the limit is $0$ and the colimit is $1$. Otherwise, the limit is $(X,\phi)$ such that for $d\in D_0$ with $F_0(d)=X$, $\phi(d)=x_i$ where $i$ is the smallest number such that $F_1(f)=x_i$ for some arrow $f$ in $D_1$ with codomain $d$. Dually, for the colimit we choose $\phi(d)=x_j$ where $j$ is the smallest number with the condition as above but domain instead of codomain.
I think it would also work with $i\in\{0,1\}$ and $x_ix_j=x_{\max(i,j)}$.
Clearly, $X$ and $0$ are not isomorphic here. Also $X\times 0\cong X$ so it seems that we need indeed more machinery to show the original claim. I think I could manage to prove it without power objects though, just in a category $E$ with finite limits, colimits and a subobject classifier $(\Omega, \true:1\to\Omega)$.
We have the pullback square $(A \xra{\id_A} A \xra{\phi_A} \Omega, A \to 1 \xra{\true} \Omega)$ from the definition of a subobject classifier with the full subobject $A$. Further, for any map $f : A \to A$, we have the commuting square $(A \xra{f} A \xra{\phi_A} \Omega, A \to 1 \xra{\true} \Omega)$ (which can be checked by introducing the diagonal $0 \to 1$, the upper triangle commutes by all maps to $1$ being equal and the lower triangle is just the pullback square from above), which means that every $f$ is a map from the limiting cone to itself, but by the universal property of the limiting cones, such a map is unique. Hence we have $A \xra{k} 0 \to A$ must be equal to the identity and $k$ is an isomorphisms.
So I basically just want to check if my counterexample and the proof are correct?
$\require{AMScd}$I'm not really sure you've defined all possible compositions in your $C$ but it looks fine. Your proof is definitely wrong since it is just saying:
This is extremely false, for example, in the topos of sets. You've misplaced the uniqueness in a pullback; there is a unique arrow $g:A\to A$ with $1_A\circ g=f$ and $A\to 1=A\overset{g}{\to}A\to1$. This is obviously true, $g=f$ is forced, but it is not saying that there is a unique arrow $g:A\to A$ full stop. You also don't need to bother with "$0\to1$", I didn't understand that point; for any $f:A\to A$, it is true that: $$\begin{CD}A@>!>>1\\@VfVV@VV\mathrm{true}V\\A@>>\phi_A>\Omega\end{CD}$$Commutes. That's because $\phi_A=\mathrm{true}\,\circ\,!$ and $!\,\circ f=\,!$. Essentially, for $\phi_A$ the pullback condition is completely trivial; it is just the statement $\phi_A=\mathrm{true}\,\circ\,!$. For general subobjects $\iota:B\hookrightarrow A$, we have that $\iota$ is the equaliser of $\phi_B$ and $\mathrm{true}\,\circ\,!$.