Abstract

I will present a version of effective topology that follows the slogan "continuous data, computable functions". In this setup we can study computable maps between topological spaces even though the spaces contain non-computable points. This is similar to effective domain theory, but more general since every countably-based T_0-space, with a chosen subbasis, appears as an object of the category of effective topological spaces.

The category of effective topological spaces can be extended to the category of effective equilogical spaces, which is locally cartesian closed, and has subset and (regular) quotient types. And when that is not enough, the category of effective equilogical spaces can be extended to the so-called relative realizability topos RT(P(N),RE).