But remember that (as far as I know) you can do intuitionist mathematics in classical mathematics, but not the other way around. So you can think of intuitionist mathematics as being embedded in classical mathematics.
The second paragraph is somewhat true --- at its base, the modern use of the term "intuitionistic logic" refers merely to not accepting the law of the excluded middle. However, there are varieties of intuitionism that are very, very inconsistent with classical logic, like those adopting the idea that "every function between real numbers is continuous".
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.
I checked the paper that I was thinking about and the condition that I saw there is distributivity being dropped rather than double negation being dropped.
There are a number of embeddings of classical logic into intuitionistic logic. The most popular/obvious is the double-negation embedding that maps a proposition to its double negation.
What you are referring to as a proposition is an element of the Heyting algebra or the Boolean algebra.
My point is something else: I don't know of a way to have a intuitionistic exterior logic and a classical internal logic.
> you can do intuitionist mathematics in classical mathematics