# Equilogical Spaces

# Submitted

### A. Bauer, L. Birkedal, D.S. 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**_{0} 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**_{0} - 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**_{0} 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**_{0} 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.
###
Table of Contents

**1. Introduction**
**2. Motivation**
**3. Equilogical Spaces**
**4. Equilogical Spaces, Type Theory and Logic**
**5. Equilogical Spaces and Domains with Totality**