[mikorym]

When you separate internal and external logic, for example in topos theory, the external logic is still classical.

For example, any topos has internal logic on subobjects of at least a Heyting algebra. In some cases you specialise to a Boolean algebra.

However, when you write things down such as your arguments around functors and constructions, you argue according to classical mathematics externally. When you enter into the category (which is chosen not to be Boolean) and argue on the subobject structure, then you are entering intuitionistic logic. This is what I mean when I say that classical logic can be argued to have intuitionistic logic embedded in it.

The cardinality of the reals being equal to the cardinality of the naturals is then something you have to construct inside the topos. So you need to construct along the spirit of a natural numbers object (perhaps a real numbers object) and then use the internal logic to argue about continuity.