This is a 🧵 about the Dedekind cut construction of real numbers in #constructiveMathematics , particularly two technical details. The first has to do with defining additive inverse and multiplication, when we can't use excluded middle for things like "is a real number positive or not?". The second is about one sided versus two sided cuts.

1/8