A Relationship between Equilogical Spaces and Type Two Effectivity
Andrej Bauer · Electronic Notes in Theoretical Computer Science · 2001
In this paper I compare two well studied approaches to topological semantics — the domain-theoretic approach, exemplified by the category of countably based equilogical spaces, Equ, and Type Two Effectivity, exemplified by the category of Baire space representations, Rep( B ). These two categories are both locally cartesian closed extensions of countably based T0-spaces. A natural question to ask is how they are related. First, we show that Rep( B ) is equivalent to a full coreflective subcategory of Equ, consisting of the so-called 0-equilogical spaces. This establishes a pair of adjoint functors between Rep( B ) and Equ. The inclusion Rep( B ) → Equ and its coreflection have many desirable properties, but they do not preserve exponentials in general. This means that the cartesian closed structures of Rep( B ) and Equ are essentially different. However, in a second comparison we show that Rep( B ) and Equ do share a common cartesian closed subcategory that contains all countably based T0-spaces. Therefore, the domain-theoretic approach and TTE yield equivalent topological semantics of computation for all higher-order types over countably based T0-spaces. We consider several examples involving the natural numbers and the real numbers to demonstrate how these comparisons make it possible to transfer results from one setting to another.