# Mathematics and Computation

## A blog about mathematics for computers

Postsby categoryby yearall

# Posts in the year 2002

### 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.

### Equilogical Spaces

With Lars Birkedal and Dana Scott.

Abstract: It is well known that one can build models of full higher-order dependent type theory (also called the calculus of constructions) using partial equivalence relations (PERs) and assemblies over a partial combinatory algebra (PCA). But the idea of categories of PERs and ERs (total equivalence relations) can be applied to other structures as well. In particular, we can easily define the category of ERs and equivalence-preserving continuous mappings over the standard category Top of topological T_0-spaces; we call these spaces (a topological space together with an ER) equilogical spaces and the resulting category Equ. We show that this category—in contradistinction to Top—is a cartesian closed category. The direct proof outlined here uses the equivalence of the category Equ to the category PEqu of PERs over algebraic lattices (a full subcategory of Top that is well known to be cartesian closed from domain theory). In another paper with Carboni and Rosolini (cited herein) a more abstract categorical generalization shows why many such categories are cartesian closed. The category Equ obviously contains Top as a full subcategory, and it naturally contains many other well known subcategories. In particular, we show why, as a consequence of work of Ershov, Berger, and others, the Kleene-Kreisel hierarchy of countable functionals of finite types can be naturally constructed in Equ from the natural numbers object N by repeated use in Equ of exponentiation and binary products. We also develop for Equ notions of modest sets (a category equivalent to Equ) and assemblies to explain why a model of dependent type theory is obtained. We make some comparisons of this model to other, known models.

Published in: Theoretical Computer Science, 315(1):35-59, 2004.