The basic picture, meet and definitions in predicative topology
by
Giovanni Sambin
The University of Padua

Any pair of sets linked by an arbitrary relation -- a minimal structure which I call a basic pair -- is sufficient to support the notions of open and of closed subset, and morevoer to show how such notions are the direct outcome of symmetry and of logical duality. The notion of continuity, and also pointfree topology, can be treated in a similar way. This approach to topological notions I have called the basic picture. It can be seen as a generalization of topology, which is obtained by addding distributivity.

To say that two subsets meet is constructively stronger than saying that they have nonempty intersection. Admitting the notion of meet, besides that of inclusion of which it is the dual, allows to characterize abstractly a relation as two (sic!) pairs of adjoint functors such that, moreover, the two left adjoint functors are connected by what I call the fundamental symmetry. Finding the ``right'' definitions in formal topology, that is topology as developed in an intuitionistic and predicative framework such as constructive type theory, is a delicate problem. The above characterization suggests a criterion: a definition in the basic picture is correct if it is expressible in category theory with the addition of meet and if it remains invariant under transfer along a relation. One can verify that all the definitions given so far in the basic picture are confirmed to be correct in this sense.

The foundational theory used is actually a tiny fragment of type theory, so that all what I obtain here is fully compatible also with topos theory.

Date received: August 11, 2001