There are plenty of countable sets of real numbers (Q and all its subsets, for one infinity), and the set of all real numbers is not countable, so there is no interpretation of the current submission title that makes sense.
It opens:
> In 1874 Georg Cantor published a theorem stating that every sequence of reals is avoided by some real, thereby showing that the reals are not countable.
> Cantor's proof uses classical logic.
> There are constructive proofs, although they all rely on the axiom of countable choice. Can the real numbers be shown uncountable without excluded middle and without the axiom of choice?
>An answer has not been found so far, although not for lack of trying.
> We show that there is a topos in which the real numbers are countable, i.e., there is an epimorphism from the object of natural numbers to the object of Dedekind reals.
> Therefore, higher-order intuitionistic logic cannot show the reals to be uncountable.
I'd argue that that set, resulting from carrying out Dedekind cuts in a particular topos, is not in fact the set of real numbers. But I also agree that it means the property of uncountability for the set of real numbers as we understand it in set theoretic terms cannot be proved intuitionistically. And I'm fine with that.
I chose that title out of a combination of deliberate clickbait, and because I felt that the original title was confusing to people who hadn't heard the abbreviation "the reals" for the set (or "space"?) of real numbers.
In other words, the object on which the existing proofs of uncountability hold and the object constructed in the talk are not necessarily the same object. In fact, the care taken by Bauer in clarifying "the object of Dedekind reals" in stating his main results leads me to believe the topos in which the Dedekind reals are countable is also a topos in which the Dedekind reals are not equivalent to other constructions of the reals.
/me not a mathematician.
/me didn't watch the video.