In [1, example C.1.2.8], a locale $Y$ (dense in another locale
$X$) without any point is given. I fail to understand the point
of such point-less locale – Why can't we identify those as the
trivial locales, and what's so great about considering locales
that have no points?
Anyway, here's the construction of $X$ and $Y$ (taken from
[1]). Let $A$ be an uncountable nonempty set (e.g. $\mathbb{R}$)
(equipped with the discrete topology), and let $X$ be the set of
all functions $\mathbb{N} \to A$, equipped with the Tychonoff
topology. For each $a \in A$, let $X_a$ be the subspace $\{f \in
X \,|\, a \in im(f)\}$, and let $$ Y = \bigcap_{a\in A} X_{a}.$$
Now the point set $Y_p$ of $Y$ is empty because there is no onto
map from $\mathbb{N}$ to $\mathbb{R}$.
In [2, section 5], Johnstone demonstrates why considering such
locales could be useful. The main argument is that topoi are
nice things to consider. However, at the point of writing, the
(external) applications of topos theory seem lacking. Hopefully
the situation has changed in mathematics in recent years. Thus
the second question: How does the consideration of pointless
locales help topos theory, and how does that in turn applies
(externally) to mathematics?
Reference
-
[1] Sketches of an Elephant: A Topos Theory Compendium [Peter
T. Johnstone] -
[2] The point of pointless topology-[Peter T. Johnstone]
Best Answer
A good answer to both questions is provided by the following variant of the Gelfand duality for commutative von Neumann algebras, which shows that the following categories are equivalent:
The category CSLEMS of compact strictly localizable enhanced measurable spaces;
The category HStonean of hyperstonean spaces and open maps.
The category HStoneanLoc of hyperstonean locales and open maps.
The category MLoc of measurable locales, defined as the full subcategory of the category of locales consisting of complete Boolean algebras that admit sufficiently many continuous valuations.
The opposite category CVNA^op of commutative von Neumann algebras, whose morphisms are normal *-homomorphisms of algebras in the opposite direction.
The first category, despite the rather complicated name, is essentially the correct category for measure theory: it incorporates equality almost everywhere, a (generalized) σ-finiteness property, and an abstract variant of the Radon measure property, which eliminate pathological measurable (and measure) spaces for which some of the most basic theorem of measure theory (such as the Riesz representation theorem or the Radon–Nikodym theorem) fail.
Of particular interest is the fourth category MLoc of mesurable locales. It is a full subcategory of the category of locales, which quite interesting: it demonstrates that both point-set general topology (as implemented by the category of topological spaces) and point-set measure theory (as implemented by the above category CSLEMS) are a part of pointfree general topology, implemented by full subcategory of the category of locales.
These parts (i.e., general topology and measure theory) are almost disjoint: locales corresponding to topological spaces are spatial, i.e., have enough points. On the other hand, points in a measurable locale are in a bijective correspondence with atoms in the original measure space. In particular, atomless measure spaces (i.e., what is typically used in practice) correspond to locales that have no points at all.
Returning to topos theory: working in the topos of sheaves of sets on a measurable locale amounts to doing ordinary mathematics in measurable families over a measurable space. For example, doing internal linear algebra in such a topos corresponds to working with measurable vector bundles, etc.