Implication Details

Claim: If a category has an initial object and is locally cartesian closed, then it has a strict initial object.

Proof: Assume that $\C$ is locally cartesian closed and $0 \in \C$ is an initial object. The slice category $\C / 0$ has a zero object, the identity of $0$. By assumption, it is also cartesian closed. But a cartesian closed category with a zero object is trivial, since for every object $A$ we have $A \cong A \times 1 \cong A \times 0 \cong 0$, where the last step uses that $A \times -$ is a left adjoint and hence preserves the initial object. Since $\C / 0$ is trivial, every morphism $X \to 0$ is an isomorphism.

This implication has a dual.