The Interval Domain in Homotopy Type Theory

Even though the real numbers are the cornerstone of many fields in mathematics, it is challenging to formalize them in a constructive setting, and in particular, homotopy type theory. Several approaches have been established to define the real numbers, and the most prominent of them are based on Dedekind cuts and on Cauchy sequences. In this paper, we study a different approach towards defining the real numbers. Our approach is based on domain theory, and in particular, the interval domain, and we build forth on recent work on domain theory in univalent foundations. All the results in this paper have been formalized in Coq as part of the UniMath library.