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).


closed as off-topic by Emil Jeřábek, cody, Damiano Mazza, Jan Johannsen, Andrej Bauer Jan 25 '18 at 7:13

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – Emil Jeřábek, cody, Damiano Mazza, Jan Johannsen, Andrej Bauer
If this question can be reworded to fit the rules in the help center, please edit the question.


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$.

  • $\begingroup$ 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. $\endgroup$ – bbarker Jan 23 '18 at 14:43

Not the answer you're looking for? Browse other questions tagged or ask your own question.