On propositional truncation in dependent type theory:
On the Dedekind real numbers via abstract Stone duality:
Andrej Bauer, Paul Taylor, The Dedekind reals in abstract Stone duality, Mathematical Structures in Computer Science 19 4 (2009) 757-838 [doi:10.1017/S0960129509007695]
Andrej Bauer, Efficient Computation with Dedekind Reals, talk at Computability and complexity in analysis 2008 and at Mathematics, Algorithms and Proofs 2008 (2008) [web, slides: pdf, extended abstract: pdf]
On the HoTT book real numbers:
Last revised on February 21, 2023 at 10:55:53. See the history of this page for a list of all contributions to it.