  It is a ubiquitous opinion among mathematicians that a real number is just a
point in the line. If this rough definition is not enough, then a mathematician
may provide a formal definition of the real numbers in the set theoretic and
axiomatic fashion, i.e. via Cauchy sequences or Dedekind cuts, or as the
collection of axioms characterizing exactly (up to isomorphism) the set of real
numbers as the complete and totally ordered Archimedean field. Actually, the
above notions of the real numbers are abstract and do not have a constructive
grounding. Definition of Cauchy sequences, and equivalence classes of these
sequences explicitly use the actual infinity. The same is for Dedekind cuts,
where the set of rational numbers is used as actual infinity. Although there is
no direct constructive grounding for these abstract notions, there are so
called intuitions on which they are based. A rigorous approach to express these
very intuition in a constructive way is proposed. It is based on the concept of
the adjacency relation that seems to be a missing primitive concept in type
theory. The approach corresponds to the intuitionistic view of Continuum
proposed by Brouwer. The famous and controversial Brouwer Continuity Theorem is
discussed on the basis of different principle than the Axiom of Continuity.
