##
What is a point-free space? Or a point-free bundle?

### Steve Vickers

Point-free spaces have been defined in various technical ways, including
as frames (locales), as formal topologies, and even - these are
"generalized spaces" - as toposes. What they have in common is that by
the time you have set up the technical framework, you have lost sight of
what the point was.

This is often misunderstood as the essence of point-free topology, and
the temptation is great to revert to point-set spaces and work with
honest points.

The problem with that comes when you look at bundles, understood as
families of spaces (the fibres) continuously indexed by base point.
Pleasant results from topos theory show that these are equivalent to
spaces internal in the topos of sheaves over the base space, but only if
you work point-free. Simple topological examples show that a point-set
approach cannot work in general. (Technically: some bundles cannot be
satisfactorily approximated by local homeomorphisms.)

I shall explain how geometric logic restores the pointwise reasoning,
but without the problems of assuming a set of points. The points of a
point-free space are the models of a geometric theory; maps between
spaces are defined using geometric constructions (colimits and finite
limits) of points; and bundles are built by geometrically constructing
theories out of points.

This underlies Grothendieck's idea of toposes as generalized spaces, and
I shall say something about how it leads to my current work using
arithmetic universes to get constructive results that are independent of
any choice of base topos.

For more details -

My 5 TACL 2017 talks
http://www.cs.bham.ac.uk/~sjv/talks.php

"Sketches for arithmetic universes"
http://www.cs.bham.ac.uk/~sjv/papersfull.php#AUSk

"Arithmetic universes and classifying toposes" (in Cahiers de topologie et géométrie différentielle catégorique)
http://www.cs.bham.ac.uk/~sjv/papersfull.php#AUClTop