Addition for lower and upper Dedekind reals

[lowasser]

Depends on #1339, but adds ~500LOC beyond that, and seems like a reasonable sub-PR to break away from #1336 .

[fredrik-bakke]

Looks good to go aside from the comment on *polymorphism. 👍

[lowasser]

We can either be forced to generalize the additive identity to every universe level, or stick with this as-is. (This comes back to the problems associated with #1334 .)

We can do that, if we want. Setting up an additive inverse for every level at least lets us use small groups on every universe level. Is that your preference?

[fredrik-bakke]

Ahh, shoot, that's a bummer. Then I think it is better to leave it as is for now. We shouldn't formalize "raise" operations on real numbers just to get this half-way polymorphism. If we really need polymorphism then the appropriate way to go would be to find the correct definition of a "large monoid" and so on, and since that is an open question for the time being, let's keep it like it is.

[lowasser]

FWIW, large monoids are probably reasonably easy; it's groups where it gets really hard. We can have those if you like.