@inbook{fab7b740ffd140fab37b8f0639d52dad,
title = "The Interval Domain in Homotopy Type Theory",
abstract = "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.",
author = "\{van der Weide\}, Niels and Dan Frumin",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.",
year = "2024",
month = may,
day = "22",
doi = "10.1007/978-3-031-61716-4\_16",
language = "English",
isbn = "978-3-031-61715-7",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "241--256",
editor = "Capretta, \{Venanzio \} and \{ Krebbers\}, \{ Robbert \} and Wiedijk, \{Freek \}",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}