 The constructive real line \(R\) as introduced above is a model of CA. Are there any other models, that is, models not isomorphic to \(R\). If classical logic is assumed, CA is a categorical theory and so the answer is no. But this is not the case within intuitionistic logic, for there it is possible for the Dedekind and Cantor reals to fail to be isomorphic, despite the fact that they are both models of CA.