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