Level-polymorphic commutative monoid of lower and upper Dedekind real numbers under addition

[lowasser]

It sounds like we don't necessarily want this, but I built this as a draft.

[fredrik-bakke]

My point on the raise operation earlier was not that it cannot be useful, but it is certainly a tedium to formalize, and its presence very often means that the setup is just insufficiently universe polymorphic. The following is not a sufficiently nuanced statement, but lately I've come to view "raise" more and more as a hack to avoid implementing the appropriate level of universe polymorphism.