Equilogical Spaces and Their Effective Version
by
Andrej Bauer
Carnegie Mellon University, School of Computer Science

An equilogical space is a T₀-space with an equivalence relation-perhaps unrelated to the topology. A morphism of equilogical spaces is an equivalence class of equivalence-preserving continuous maps. The category of equilogical spaces Equ proves to be cartesian closed and, of course, contains the category of T₀-spaces as a full subcategory. This definition and the basic result was found by Dana Scott in late 1996.

The inclusion of categories mentioned preserves products, as well as all exponentials that already exist in T₀-spaces. The category Equ also contains many interesting subcategories. For example, Reinhold Heckmann showed recently that one version of the category of filter spaces, which is another cartesian closed extension of T₀-spaces, is a full subcategory of Equ.

By considering only countably based T₀-spaces together with a given choice of subbasis and by appropriately restricting the notion of morphisms, we obtain the category of effective equilogical spaces, which is again cartesian closed. In a certain sense the category contains all countably based T₀-spaces but, remember, only computable morphisms. The category actually extends to the so-called computability topos, which is a kind of realizability topos. The usefulness of the definition is that we can now study computability on many classical spaces in a type-theoretically and logically rich setting, even though the spaces are uncountable and contain non-computable points.

Logics of Types and Computation at CMU

Date received: June 8, 1999