Constructive analysis in UTT (presentation in Darmstadt)

Posted on 2018-02-01

It is not possible to exhibit information about real numbers such as Dedekind reals or (quotiented) Cauchy reals (as opposed to Bishop-style Cauchy reals), because, for example, there are no non-constant functions into observable types such as the booleans or the integers. We overcome this by considering real numbers equipped with additional structure, which we call locators. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy approximation. Such constructions are reminiscent of computable analysis. However, instead of working with a notion of computability, we simply work constructively to extract observational information.