<p>The coproduct is the <em>disjoint</em> union. Set-theoretically, you can think of forming the coproduct of the sets $A$ and $B$ as: </p>

<p>$$
 A + B \;\;\triangleq\;\; \{ (0, a) \;|\; a \in A \} \cup \{ (1, b) \;|\; b \in B \}
$$</p>

<p>Now it should be obvious that $A + A \not= A$.</p>

CC BY-SA 3.0
2018-01-23T14:43:54.210Z
Thanks, I see now; "disjoint unions" were also used to describe dependent pair types, but I guess in that case there is a judgementally defined dependence on the second element, whereas for coproducts it is a simple label that is applied.
bbarker
CC BY-SA 3.0
2018-01-23T14:07:25.917Z
2018-01-23T14:07:25.917Z
Neel Krishnaswami
<p>In the HoTT book, it is said</p>

<blockquote>
  <p>The type of booleans <em>2 : U</em> is intended to have exactly two elements. It is clear that we could construct this type out of coproduct and unit types as <strong>1 + 1</strong>.</p>
</blockquote>

<p>I don't see how this works, since it seems to me <strong>A + A = A</strong>, which would imply <strong>1 + 1 = 1</strong>, and <strong>1 != 2</strong>. What am I missing?  (Sorry for the brevity; I'm only able to work and read using a mobile device for this week).</p>

<type-theory><homotopy-type-theory>
What is the coproduct: A + A?
bbarker
# What is the coproduct: A + A?

(Asked by: username_0 on 2018-01-23)

In the HoTT book, it is said

> The type of booleans *2 : U* is intended to have exactly two elements. It is clear that we could construct this type out of coproduct and unit types as **1 + 1**.

I don't see how this works, since it seems to me **A + A = A**, which would imply **1 + 1 = 1**, and **1 != 2**. What am I missing? (Sorry for the brevity; I'm only able to work and read using a mobile device for this week).

**Tags:** type-theory, homotopy-type-theory

---

## 1 answers

### Answer by username_1 on 2018-01-23. Score: 3 | Accepted answer

The coproduct is the *disjoint* union. Set-theoretically, you can think of forming the coproduct of the sets $A$ and $B$ as:

$$
A + B \;\;\triangleq\;\; \{ (0, a) \;|\; a \in A \} \cup \{ (1, b) \;|\; b \in B \}
$$

Now it should be obvious that $A + A \not= A$.

> **Comments:**
> **username_0**: Thanks, I see now; "disjoint unions" were also used to describe dependent pair types, but I guess in that case there is a judgementally defined dependence on the second element, whereas for coproducts it is a simple label that is applied.  

---

