Analysis and the real numbers tend to be very hard to encode in constructive foundations. We still haven't got the right balance between checking for computabi

Analysis and the real numbers tend to be very hard to encode in constructive foundations. We still haven't got the right balance between checking for computability of the proof and all objects it hypothesizes, versus letting some of the types we hypothesize over be uncomputable and uncountably large, while requiring that propositional types (squash types) have continuous elements.