So I also should probably show that we actually have naturality for the natural isomorphisms (not just that these morphisms exist, but that they form natural transformations). But the proof is straight forward, here's the unitors. Naturality here means that given \\(f : x \to y\\), this diagram commutes:

\[\begin{matrix}\mathbf{0} + x & \cong & x & \cong & x+ \mathbf{0} \\\ [i_\mathbf{0} ,f] \downarrow & & f\downarrow & & \downarrow [f,i_\mathbf{0}] \\\ \mathbf{0} + y & \cong & y &\cong& y + \mathbf{0} \end{matrix}\]

where the morphisms on the sides always exist due to the universal properties of the coproduct and initial objects.

\[\begin{matrix}\mathbf{0} + x & \cong & x & \cong & x+ \mathbf{0} \\\ [i_\mathbf{0} ,f] \downarrow & & f\downarrow & & \downarrow [f,i_\mathbf{0}] \\\ \mathbf{0} + y & \cong & y &\cong& y + \mathbf{0} \end{matrix}\]

where the morphisms on the sides always exist due to the universal properties of the coproduct and initial objects.