# A Relationship between Equilogical Spaces and Type Two Effectivity

Abstract: 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, omegaEqu, 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 T_0-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 omegaEqu, consisting of the so-called 0-equilogical spaces. This establishes a pair of adjoint functors between Rep(B) and omegaEqu. The inclusion of Rep(B) in omegaEqu 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 omegaEqu are essentially different. However, in a second comparison we show that Rep(B) and omegaEqu do share a common cartesian closed subcategory that contains all countably based T_0-spaces. Therefore, the domain-theoretic approach and TTE yield equivalent topological semantics of computation for all higher-order types over countably based T_0-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.

Published in: Mathematical logic quarterly, 2002, vol. 48, suppl. 1, 1-15.

Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.