What makes a map f: X -> Y continuous? That means that if you jiggle the argument x around a little - not too much - to neighbouring points, then the result f(x) won't make any sudden jumps. Obviously, to make that precise, you have to give more meaning to "jiggle around" and "neighbouring".
Most mathematicians say that you take a set like X and then specify that some subsets are "open". This means that every element of the open subset also has some jiggle room around it, still within the open subset. The structure of X, together with the specification of which subsets are open, is then a point-set topological space. Once both X and Y have that structure, continuity means that for each open subset V containing f(x), there is some jiggle room round x within which the result is still in V; and this is witnessed by an open subset U containing x and with f(U) included in V.
This definition has been broadly accepted through most of the 20th century, but since perhaps the 60s there has been growing recognition of problems with taking X and Y as sets equipped with extra structure. In a mathematics founded on set theory, the default assumption is that all collections are sets (with the exception of some, proper classes, that are known to be "too big"). However, this becomes much more delicate if you want to consider "variable sets" X(z), parametrized by points z of some other topological space Z. Obviously it would be nice to just "do topology" with these, by sprinkling parameters z everywhere, but that doesn't really work with the point-set definition. The problem is that there are variable spaces we should like to capture that don't have satisfactory variable sets for their points.
A solution is provided by point-free topology. Here we don't assume that the collection of points X can be represented satisfactorily as a set. In fact we don't assume it is known until we have described the topology. The way this works is to consider each open U not as a set of points, but as a logical property "x in U" that is meaningful for the points (whatever the points are). In this style, some interactions between the opens, which previously were implicit in the knowledge of what the points were, have to be stated explicitly as logical axioms. Once that is done, we have a logical theory, and the points can now be defined as its models.
The logic that must be used, the so-called geometric logic, is a bit unusual, and arises out of Grothendieck's topos theory. One illuminating way to view it, which comes out of ideas (Abramsky, Smyth) of the role of topology in computer science, is that it is a logic of what you can actually observe. I used that as the basis of my book "Topology via Logic" (also, in more detail, the article "Issues of logic, algebra and topology in ontology"). We can now define -
A point-free topological space is a geometric theory. Its points are the models of that theory.
A key aspect of this is that the theory may be a first-order theory. This insight lies right at the heart of topos theory, because the same definition then admits some point-free spaces, the toposes, that vastly generalize the old point-set ones. For example, the class of sets becomes a point-free space (the "object classifier"). The geometric logic then gives rise to a geometric mathematics, and it turns out that continuity depends on restricting oneself to that geometric mathematics.
A continuous map from X to Y is a construction, within geometric mathematics, of points of Y out of points of X.
Much mathematics has already been accomplished in this geometric style. How much more can be done, and in particular how much topos theory, is still an open question that invites further exploration.
As I mentioned, much of my work investigates how ordinary mathematics can be done in geometric logic. The underlying problem is that a point-free space may really not have enough points. In logical terms (point = model of a theory), this is because geometric theories may be incomplete. But that shortage of points is only if the models are sought in ordinary sets. There will always be enough points if you are prepared to seek models in non-standard sets (i.e. in the internal mathematics of toposes). The advantage of geometric logic is that it applies equally well in all those non-standard universes, and transports cleanly between them (technically: it is preserved by inverse image functors of geometric morphisms). Hence by reasoning geometrically you cover also these non-standard points, and of them there are enough.
Many of the ideas are set out in Topical categories of domains, which investigates results known from domain theory and the semantics of computer programming languages (in particular, the results of Samson Abramsky's logical approach). It uses geometric logic to exploit in a deep way the idea of classifying toposes as spaces of points.
An important tool is the theory of powerlocales, or "point-free hyperspaces". (A hyperspace is a space whose points are subspaces of some other space. As powerdomains they have proved an effective tool for discussing non-determinism in computation, since the result of a function then may be a subspace of points rather than a single point.) These give a powerful way to discuss issues such as compactness and I have used them throughout my work. Their good interaction with geometric logic is described in detail in The double powerlocale and exponentiation, which investigates Martin Hyland's famous result from point-free topology on the ability to construct spaces of maps (and, technically, on local compactness).
One important consequence of the infinitary disjunctions in geometric logic is that there is a "geometric type theory" to go with it. An interesting question, proposed in Topical categories of domains and discussed in Locales and toposes as spaces, concerns what happens if one combines some of the type theory with the finitary geometric logic, i.e. coherent logic. This is an "arithmetic" logic, and corresponds to using Joyal's arithmetic universes as a substitute for Grothendieck toposes. Though it is formally less powerful than geometric logic, it is at least strong enough to cover real numbers and leads to a constructive logic that does not depend on choosing a base elementary topos "of sets".
Grothendieck topos theory might be characterized as "generalized point-free topology", where the generalization is to spaces of models of non-propositional geometric theories, and consequently the point-free approach has to shift from lattices (of opens) to categories (of sheaves). See my TACL talks 1-4.
The methodology then is that a space is a Grothendieck topos (the category of sheaves), and a continuous map is a geometric morphism. However, a the category of sheaves has to be based on a given category of sets. That could be any elementary topos with natural numbers object, not necessarily the classical sets; but the fact of having to choose is itself a nuisance that makes it harder to be foundationally robust.
The AU dream is to state and prove topological results in a constructive, foundationally robust way that does not depend on choosing a base topos (or a base anything). See my TACL talks 5.
At present we are a long way from realising that dream in algebraic topology, which presents big challenges. Grothendieck used toposes as a place in which to do sheaf cohomology, and those techniques would certainly not work unmodified with AUs.
See -
Also, for a good report on the basic ideas as known in 1996, see Alan Morrison's MSc dissertation "Reasoning in Arithmetic Universes".
I am now retired from Birmingham University, though I still take part in research activities of the Theory Group. In principle, as an honorary member of staff, I can still supervise PhD students. However, it is most unlikely that there would be any university funding available for it.