There are some significant mathematical points that can be made in response to Vasili Galchin's question about the "constructive" existence of Cantor space, but I fear that these are going to get lost in the cross-fire of comments that neither state their background assumptions nor lay out the mathematics. It is well over a century since we discovered that it is meaningless to talk about the absolute truth or falsity of (semantical) statements in mathematics. There are many many people and foundational positions that call themselves "constructive". Unfortunately the experts in these theories have a tendency to assert a monopoly on the word, and ignore the existence of the other points of view, whilst non-experts repeat half-remembered and mis-understood opinions that may originate from the opponents and not the proponents of the theories. On the other hand, Peter Schuster and Giovanni Sambin have made some effort in recent years to bring these disciplines together. I am not going to attempt to make a list of "constructive" theories, and I would strongly advise against referring to such lists elsewhere, ESPECIALLY in Wikipedia. Nor am I going to try to represent positions other than my own -- I invite the respective experts to do this. Traditionally, Cantor space is described as a subspace of R or [0,1] using the "middle third" construction, but I learned it like that long before I became a constructivist of any kind, so I don't know whether there are any constructive subtleties associated with this view. I think of Cantor as the exponential 2^N, so FOR EXAMPLE it makes sense to talk about it in any CCC, or a topos. However, the interesting question is what it looks like as a TOPOLOGICAL SPACE, in the many different interpretations of that phrase. We can do topology starting from the points, or starting from the open sets. In the latter case, these have a basis whose members are named by FINITE sets of integers: a point of Cantor space is a decidable (possibly) infinite set of integers, and lies in a basic open set if the infinite set includes the finite one. The first interesting mathematical question is this: if we define Cantor space starting from its points, but take these to be given by TOTAL RECURSIVE FUNCTIONS N-->2, and then put the topology that I have just mentioned on it, what are the properties of this topology? In particular, is it compact? The answer is no, because of the "Kleene Tree". This is a computably defined infnite tree that has no infinite computable path. There are many descriptions of this, including one by Andrej Bauer: math.andrej.com/2006/04/25/konigs-lemma-and-the-kleene-tree/ The second interesting mathematical point is that, by looking at the open sets instead of the points as our formulation of topology, the answer is different. The whole of this discussion can be conducted using the closed real interval in place of Cantor space, so many things are better documented in the literature for one example rather than the other. In particular, compactness of the interval has more careful descriptions in: LOCALE THEORY: Michael Fourman and Martin Hyland, "Sheaf models for analysis", in Michael Fourman, Chris Mulvey, and Dana Scott, editors, "Applications of Sheaves", number 753 in Lecture Notes in Mathematics, pages 280--301. Springer-Verlag, 1979. FORMAL TOPOLOGY: Jan Cederquist and Sara Negri, "A constructive proof of the Heine--Borel covering theorem for formal reals", in Stefano Beradi and Mario Coppo, editors, "Types for Proofs and Programs", number 1158 in Lecture Notes in Computer Science, page 6275. Springer-Verlag, 1996. ABSTRACT STONE DUALITY: Andrej Bauer and Paul Taylor, "The Dedekind reals in abstract Stone duality", www.PaulTaylor.EU/ASD/dedras I wrote a sketch (not a properly written paper) about the construction of Cantor Space in ASD and its compactness in "Tychonov's Theorem in ASD", www.PaulTaylor.EU/ASD/misclc.php#tyctas Paul Taylor PS Please refer to my website as paultaylor.eu, not monad.me.uk, as it will be moving home shortly, and I will be better able to ensure continuity of service for the name paultaylor.eu, whilst I would like to discontinue monad.me.uk at some stage.