Interestingly, constructive mathematics cannot prove that the Cauchy and Dedekind constructions are isomorphic: "As often happens in an intuitionistic setting,

Interestingly, constructive mathematics cannot prove that the Cauchy and Dedekind constructions are isomorphic: "As often happens in an intuitionistic setting, classically equivalent notions fork. Dedekind reals give rise to several demonstrably different collections of reals when only intuitionistic logic is assumed" https://arxiv.org/pdf/1510.00641 https://arxiv.org/pdf/1510.00641