1
$\begingroup$

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

$\endgroup$

closed as off-topic by Emil Jeřábek supports Monica, 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 supports Monica, 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.

3
$\begingroup$

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

$\endgroup$
  • $\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.