  The real numbers are important in both mathematics and computation theory.
Computationally, real numbers can be represented in several ways; most commonly
using inexact floating-point data-types, but also using exact
arbitrary-precision data-types which satisfy the expected mathematical
properties of the reals. This thesis is concerned with formalising properties
of certain types for exact real arithmetic, as well as utilising them
computationally for the purposes of search, optimisation and regression.
  We develop, in a constructive and univalent type-theoretic foundation of
mathematics, a formalised framework for performing search, optimisation and
regression on a wide class of types. This framework utilises Mart\'in
Escard\'o's prior work on searchable types, along with a convenient version of
ultrametric spaces -- which we call closeness spaces -- in order to
consistently search certain infinite types using the functional programming
language and proof assistant Agda.
  We formally define and prove the convergence properties of type-theoretic
variants of global optimisation and parametric regression, problems related to
search from the literature of analysis. As we work in a constructive setting,
these convergence theorems yield computational algorithms for correct
optimisation and regression on the types of our framework.
  Importantly, we can instantiate our framework on data-types from the
literature of exact real arithmetic, allowing us to perform our variants of
search, optimisation and regression on ternary signed-digit encodings of the
real numbers, as well as a simplified version of Hans-J. Boehm's functional
encodings of real numbers. Furthermore, we contribute to the extensive work on
ternary signed-digits by formally verifying the definition of certain exact
real arithmetic operations using the Escard\'o-Simpson interval object
specification of compact intervals.
