<p>Firstly, the HoTT book does not succumb to the reductionist ideas that often occlude important structure. Just because we can simulate <span class="math-container">$X$</span> using <span class="math-container">$Y$</span> that does not mean we should define <span class="math-container">$X$</span> using <span class="math-container">$Y$</span>.</p>
<p>Having said that, your suggestion is to simulate <span class="math-container">$A + B$</span> as the sum <span class="math-container">$\sum_{n : \mathbb{N}} C(n)$</span> where
<span class="math-container">$$
C(n) = \begin{cases}
A &amp; \text{if $n = 0$}\\
B &amp; \text{if $n \neq 0$}
\end{cases}
$$</span>
This is not correct because it gets you the sum <span class="math-container">$A + B + B + B + B + \cdots$</span>. Instead we want
<span class="math-container">$$
C(n) = \begin{cases}
A &amp; \text{if $n = 0$}\\
B &amp; \text{if $n = 1$}\\
\mathsf{Empty} &amp; \text{if $n &gt; 1$}\\
\end{cases}
$$</span>
Note that the type you get is not equal to <span class="math-container">$A + B$</span> but only equivalent to it. Using it instead of <span class="math-container">$A + B$</span> brings in a significant overhead, as you always have to dispense with the third case <span class="math-container">$n &gt; 1$</span>. We can improve the construction by using booleans instead of natural numbers, as we have
<span class="math-container">$$A + B \simeq \sum\nolimits_{n : \mathsf{Bool}} D(b)$$</span>
where <span class="math-container">$D(\mathsf{false}) = A$</span> and <span class="math-container">$D(\mathsf{true}) = B$</span>. (You may find <a href="https://cstheory.stackexchange.com/a/25853/705">this answer</a> useful as well.)</p>
<p>The moral of the story is that the coproduct types are <em>not</em> &quot;redundant&quot;, but it is <em>useful</em> to know that they are expressible equivalently in terms of booleans and dependent sums.</p>

CC BY-SA 4.0
2021-08-21T09:19:44.880Z
2021-08-21T09:43:32.090Z
2021-08-21T09:43:32.090Z
Andrej Bauer
<p>In the homotopy type theory book section A.2.5 defines <span class="math-container">$\Sigma$</span>-types, A.2.6 coproduct types and A.2.9 the natural numbers type.</p>
<p>If we already have <span class="math-container">$\Sigma$</span>-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?</p>

<type-theory>
Are coproduct types redundant in presence of natural numbers and $\Sigma$-types?
yelena
# Are coproduct types redundant in presence of natural numbers and $\Sigma$-types?

(Asked by: username_0 on 2021-08-21)

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?

**Tags:** type-theory


---

## 1 answers

### Answer by username_1 on 2021-08-21. Score: 3

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](https://cstheory.stackexchange.com/a/25853/705) 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.


---

