A notion of the real numbers which is constructed as an initial interval object.
Martín Escardó and Alex Simpson. A universal characterization of the closed Euclidean interval. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, pages 115–125. IEEE Computer Society, 2001. (doi:10.1109/LICS.2001.932488, pdf)
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Auke Booij, Analysis in Univalent Type Theory (2020) [etheses:10411, pdf, pdf]
Created on December 26, 2023 at 06:51:32. See the history of this page for a list of all contributions to it.