hott-reals Chapter 11.3 of the HoTT book, in Cubical Agda https://homotopytypetheory.org/book/ https://github.com/agda/cubical Poster Quick overview from the 2026 PhD Open House at University of Utah: https://users.cs.utah.edu/~blg/resources/pdf/jackson-phdopenhouse-2026.pdf