CPP 2017: Formalising Real Numbers in Homotopy Type Theory Paper: https://dx.doi.org/10.1145/3018610.3018614 Slides: http://thedragonrider.free.fr/CPP2017slides.pdf