If the classical definition of topological space is analysed at the light of an intuitionistic and predicative foundation
as Martin-Löf’s type theory, one is lead to the notion of basic pair: a pair of sets, concrete points and observables (or
formal neighbourhoods), linked by a binary relation called forcing. The new discovery is that this is enough to introduce
the topological notions of open and closed subsets, both in the concrete (pointwise) and in the formal (pointfree) sense.
Actually, a new rich structure arises, consisting of a symmetry between concrete and formal and of a logical duality between
open and closed. Closed subsets are defined primitively, as universal-existential images of subsets along the forcing relation,
while open subsets are existential-universal images. So, in the same way as logic gives a theory of subsets as the extension
of unary propositional functions over a given set, now logic is seen to produce topology if we pass to two sets linked by
a relation, that is a propositional function with two arguments.
Usual topological spaces are obtained by adding the condition that the extensions of observables form a base for a topology,
which is seen to be equivalent to distributivity. Formal topologies are then obtained by axiomatizing the structure induced
on observables, with some improvements on previous definitions. A morphism between basic pairs is essentially a pair of relations
producing a commutative square: this is thus the essence of continuity. Usual continuous functions become a special case.
This new perspective, which is here called basic picture, starts a new phase in constructive topology, where logic and topology
are deeply connected and where the pointwise and the pointfree approach to topology can live together. It also brings to the
development of topology in a more general, nondistributive sense.