In the homotopy type theory book section A.2.5 defines $\Sigma$-types, A.2.6 coproduct types and A.2.9 the natural numbers type.
If we already have $\Sigma$-types and the natural numbers type can we emulate coproduct types by sending 0 to the left summand and the positive natural numbers to the right summand? So coproducts are not strictly necessary then?
Firstly, the HoTT book does not succumb to the reductionist ideas that often occlude important structure. Just because we can simulate $X$ using $Y$ that does not mean we should define $X$ using $Y$.
Having said that, your suggestion is to simulate $A + B$ as the sum $\sum_{n : \mathbb{N}} C(n)$ where $$ C(n) = \begin{cases} A & \text{if $n = 0$}\\ B & \text{if $n \neq 0$} \end{cases} $$ This is not correct because it gets you the sum $A + B + B + B + B + \cdots$. Instead we want $$ C(n) = \begin{cases} A & \text{if $n = 0$}\\ B & \text{if $n = 1$}\\ \mathsf{Empty} & \text{if $n > 1$}\\ \end{cases} $$ Note that the type you get is not equal to $A + B$ but only equivalent to it. Using it instead of $A + B$ brings in a significant overhead, as you always have to dispense with the third case $n > 1$. We can improve the construction by using booleans instead of natural numbers, as we have $$A + B \simeq \sum\nolimits_{n : \mathsf{Bool}} D(b)$$ where $D(\mathsf{false}) = A$ and $D(\mathsf{true}) = B$. (You may find this answer useful as well.)
The moral of the story is that the coproduct types are not "redundant", but it is useful to know that they are expressible equivalently in terms of booleans and dependent sums.
