Chapter 3: sums are tagged unions

[nbloomf]

In chapter 3, definition 3 and the subsequent examples, I think it'd be helpful to note that for values of a sum type $A \mid B$ it is also possible to tell which summand the value came from. I've heard sums described as tagged unions for this reason -- each value has a tag that tells us which summand it belongs to. (In Haskell these are the constructors Left and Right.)

This is especially important for sums like $A \mid A$. If $a : A$ and we think of $a$ as having type $A \mid A$ as well, how do we tell which copy of $A$ $a$ came from?

[bor0]

I think your explanation in e3592d0 (line 125) fixes this, thanks!