Equilogical spaces.
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. 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 Top0 of topological T0-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 Top0--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 Top0 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 Top0 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.
Introduction
The genesis of this paper is the manuscript [35] "A New Category?" privately
circulated by Dana Scott in December of 1996. During the last part of his
Supported in part by U.S. National Science Foundation Grant CCR-9409997.
Preprint submitted to Elsevier Preprint 29 September 1998
graduate course on Domain Theory he had realized that by using some basic
and well-known properties of domains (specifically, algebraic lattices) the category
of equivalence relations on T 0 -spaces not only was an extension of the
topological category but was cartesian closed.
The present paper incorporates original motivation, definitions, and proofs of
the earlier manuscript, and we then give an equivalent definition suggesting
relationships to the extensive work on partial equivalence relations over partial
combinatory algebras (hereafter, PCAs). In our conference paper [6], the
reader will find an abstract framework due to Carboni and Rosolini in which
the categories of equilogical spaces and partial equivalence relations over PCAs
fit. Indeed, it is shown that there is a larger category than that of equilogi-
cal spaces that is cartesian closed. However, we shall not discuss the abstract
categorical framework here (namely, that of exact completions of categories).
As in the earlier manuscript, our desire here is to give a fairly concrete description
of the structures involved and the constructions from them. By extending
the first treatment, we use an alternate equivalent definition of the category
of equilogical spaces to give a definition of a model of dependent type theory
and logic, analogous to the work over PCAs. We also discuss how far that
analogy extends.
The final section of the paper shows how the work of Y. Ershov and E. Berger
concerning the Kleene-Kreisel hierarchy of countable functionals and extensions
can be incorporated into the category of equilogical spaces. In terms of
the type theory, it turns out that the higher types over the integers N ! N ,
are indeed the countable
functionals, as expected. In order to see this, we have to add appropriate
categorical definitions to Berger's work.
Motivation
The familiar categories Set and Top, consisting of sets and arbitrary mappings
and of topological spaces and continuous mappings, have many well known closure
properties. For example, they are both complete and cocomplete, meaning
that they have all (small) limits and colimits. They are well-powered and co-
well-powered, meaning that collections of subobjects and quotients of objects
can be represented by sets. They are also nicely related, since Set can be
regarded as a full subcategory of Top, and the forgetful functor that takes
a topological space to its underlying set preserves limits and colimits (but
reflects neither).
The category Set is also a cartesian closed category, meaning that the function-
space construct or the internal hom-functor is very well behaved, in the sense
that the functor \Delta \Theta B is adjoint to objects B. However, it has
been known for a long time that in Top no such assertion is available, because
in general it is not possible to assign a topology to the set of continuous functions
making this adjointness valid-except under some special conditions on
the space B. Many remedies have been proposed, notably, (a) cutting down
to compactly generated spaces, or (b) expanding the category to the category
of filter spaces (or a related kind of limit space). These are interesting sugges-
tions, but both have some drawbacks. Suggestion (a) applies only to Hausdorff
spaces, and suggestion (2)-which the authors consider the more interesting
from a logical point of view-introduces very unfamiliar spaces at the higher
types (i.e., after iterating the function-space construct several times). It remains
to be seen whether the suggestion of this paper can be regarded as more
concrete or more helpful than either (a) or (b).
Our solution to the problem of cartesian closedness is motivated by domain
theory. The new category is formed from the category Top 0
of topological
-spaces by using spaces together with arbitrary equivalence relations, to
form the category, to be called called Equ, where the mappings are (suitable
equivalence classes of) continuous mappings which preserve the equivalence
relations. more precise definition will be given below.) Let us call these
spaces equilogical spaces and the mappings equivariant. It seems surprising
that this category has not been noticed before-if in fact it has not. It is easy
to see that Equ is complete and cocomplete and that it embeds Top 0
as a full
and faithful subcategory (by taking the equivalence relation to be the identity
relation).
What is perhaps not so obvious is that Equ is indeed cartesian closed. The
proof of cartesian closedness outlined here uses old theorems in domain theory
originally discovered by Scott: in particular, an injective property of algebraic
lattices treated as topological spaces and the fact that they form a cartesian
closed category (along with continuous functions). A more abstract, categorical
proof can be found in [6] or in [34]. Also, in Section 4 we give an alternative
concrete proof. Of course, algebraic lattices are just one of many cartesian
closed categories proposed for domain theory-and not the most popular one.
They allow, however, for some helpful embeddings of T 0 -spaces.
For a long time Scott has been distressed that there are too many proposed
categories of domains and that their study has become too arcane. It was
hoped that the idea of synthetic domain theory would be the natural solution-
but that theory has been slowed by many technical problems. The related idea
of axiomatic domain theory is likewise hampered by the need to overcome
technical difficulties. Despite very good work in both these directions, he does
not feel that a final theory has emerged. Perhaps some of the ideas that have
been used in these other approaches can be transplanted to the study of Equ,
which seems to be a rich and fairly natural category with many subcategories.
The basic idea of the synthetic approach is to establish a typed -calculus
once and for all, and then to single out useful types (or domains) by means of
special properties-just as is done in several other branches of mathematics.
As far as Equ is concerned, the possibilities seem good, but this is still work
in progress. We are encouraged, however, by the results so far obtained, some
of which are presented here.
3 Equilogical Spaces
We begin by defining some notation and calling to mind some basic definitions
and theorems concerning T 0 -spaces and algebraic lattices. We then turn to the
definition of equilogical spaces.
-Spaces and Algebraic Lattices.
Topological spaces will be considered as structures
the set of points of the space, and
where\Omega T is the set of open sets of T . We
shall often write jT so as not to have to use a special letter for the points
of a space. Complete lattices (and, more generally, posets) will be considered
as structures is the partial ordering of the set jLj.
Completeness of course demands that every subset S ' jLj has a least upper
bound W S 2 jLj.
Definition 3.1 The neighborhood filter of a point x 2 jT j of a topological
space T is defined by the equation:
The spaces we shall be concerned with are the T 0 -spaces, where the topology
distinguishes the points.
Definition 3.2 A topological space is a T 0 -space provided that for every
pair of distinct points there is an open set that contians one but not the
other. Another way to say this condition is to say that for all x; y 2 jT j, if
y. The category of all such spaces and continuous
mappings between them is denoted by Top 0 .
Definition 3.3 The specialization ordering of a topological space T is
defined by:
for all x; y 2 jT j.
Definition 3.4 Let L be a complete lattice. The \Sigma-topology on the lattice
is defined as the collection of all upward closed subsets U ' jLj such that
The collection of all such subsets is denoted by \Sigma L .
The following theorems are now well-known. Proofs can, e.g., be found in [12].
Theorem 3.5 Given a complete lattice L, the structure hjLj; \Sigma L i is a T 0 -space
whose specialization ordering is exactly -L .
For the powerset spaces PA the \Sigma-topology is very easy to describe: the open
sets U ' PA are the families of "finite character"; that is, a subset X ' A
belongs to U if, and only if, some finite subset of X belongs to U . This is the
same as giving PA the topology that corresponds to the product topology
on 2 A where the two-element set has the topology with one open point and
one closed point. The powerset spaces have an important role as being able to
embed every T 0 -space. The following elementary result is key to the subsequent
development.
Theorem 3.6 (The Embedding Theorem) Given a T 0 -space T , the mapping
x 7! T (x) is a topological embedding of T into
P\Omega T considered as a space
with the \Sigma-topology.
Powerset spaces also have another important property concerning continouous
functions which allows for the transfer of functions over to the powerset space.
Theorem 3.7 (The Extension Theorem) If Y is a subspace of a topological
space X , and if f continuous, then the function f has a
continuous extension to all the points of X .
Scott noticed the above theorems in 1970/71 and also pointed out that it in
fact holds for all continuous retracts of the powerset spaces-these are the
continuous lattices-but for our purposes here, the above suffices.
Powerset lattices can be generalized to algebraic lattices, namely those complete
lattices that can be represented isomorphically as complete sublattices
of a powerset closed under arbitrary intersections and directed unions. (These
lattices can be characterized in other ways as well; see, e.g., [9,12].) The \Sigma-
topology on an algebraic lattice is just the restriction of the topology of the
powerset space. An algebraic lattice is a continuous retract of the powerset
containing it, but not all such retracts are algebraic.
The reason for considering algebraic lattices is that the lattice of continuous
functions between powerset spaces is not usually a powerset space, but it is
an algebraic lattice. And this extends to all algebraic lattices. Hence, we have
the well known theorem (see [9,12]):
Theorem 3.8 The category ALat is cartesian closed.
The Category of Equilogical Spaces.
We have now reviewed sufficient material to be able to give two definitions
of the category of equilogical spaces and to show that the two definitions are
equivalent. We will then prove that the category is cartesian closed.
Definition 3.9 The category Equ of equilogical spaces is defined as follows

(1) Objects are structures
is an (arbitrary) equivalence relation on the set jEj.
(2) The mappings between equilogical spaces are the equivalence classes of
continuous mappings between the topological spaces that preserve the
equivalence relation (equivariant mappings), where the equivalence relation
on mappings is defined by
We remark that it has to be proved that j E!F actually is an equivalence
relation, but this is an elementary exercise. It also has to be proved that the
equilogical spaces and equivariant maps form a category, but this can also be
safely left to the reader.
One odd feature of this definition is that the equivalence relation of an equi-
logical space may have very little to do with the topology. This means that
in some cases the only equivariant mappings between two spaces might be
the constant maps, or the only automorphisms of a given space might be the
identity-despite a rich underlying topology. Thus, future investigations may
suggest limiting the equivalence relations. But, for now, the general properties
of the category seem to work out well for arbitrary equivalence relations, so
we have not been motivated to make any further restrictions in this paper.
Recall that a category is complete if it has all (small) products and equalizers
of all pairs of parallel arrows. Similarly, a category is cocomplete if it has all
(small) coproducts and coequalizers of all pairs of parallel arrows. Also recall
that a regular subobject is a subobject which arises as the equalizer of a pair
of parallel arrows and that a category is regular well-powered if the regular
subobjects of every object constitute a set. Similarly, a regular quotient is
a qoutient which arises as the coequalizer of a pair of parallel arrows and a
category is regular co-well-powered if no object has a proper class of non-isomorphic
regular quotients.
Theorem 3.10 The category Equ is complete, cocomplete, and it is regular
well-powered, and regular co-well-powered. 4
Proof. The proof proceeds along standard lines making use of the corresponding
properties of topological spaces.
Take products first. The product (of any number) of topological spaces is a
space with a product topology. The product of equivalence relations is an
equivalence relation. The projection mappings are clearly equivariant. And,
if we have a family of (equivalence classes of) equivariant mappings into the
4 The authors are indebted to Peter Johnstone for pointing out that, contrary to
the assertion made in Scott's original unpublished manuscript, Equ is not well
powered, for there are fairly simple examples of objects in the category with an
unbounded number of non-isomorphic subobjects.
various factor spaces, then (after applying the Axiom of Choice to pick repre-
sentatives) we can obtain in the usual way one equivariant mapping into the
product that combines all the separate mappings.
Next, take equalizers. Suppose f; are two (representatives of)
equivariant mappings. Form the set f x 2 jEj j f(x) jF g(x) g. Endow this set
with the subspace topology and with the restriction of the equivalence relation
This structure, along with the obvious inclusion mapping into E, is the
desired equailizer. Thus, Equ is a complete category.
On to coproducts. The coproduct of topological spaces is just a disjoint union
of the underlying sets with the topology on the union generated by the union
of all the topologies. For equivalence relations, we have only to note that the
union of equivalence relations on disjoint sets is indeed an equivalence relation.
The injection mappings from the separate spaces into the union are obvious,
as well as is the lifting property of a family of mappings from the separate
spaces into a given target space.
Next, we discuss coequalizers. Suppose f; are two (representatives
of) equivariant mappings. On jF j we form the least equivalence relation containing
both jF and the set of pairs f (f(x); g. Using the
same topological space as F does and this equivalence relation, we form the
equilogical space G. There is an obvious equivariant mapping c G. This
structure G, along with the mapping c, is the desired coequailizer. Thus, Equ
is a cocomplete category.
Finally, we turn to well-poweredness. The properties of being regular well-
powered and regular co-well-powered follow from the corresponding properties
of Top 0 and the category of equivalence relations. But, one has to be careful to
check that the regular subobjects are obtained by selecting some equivalence
classes and taking the union of them to form a subspace; likewise, forming
a regular quotient is just making the equivalence relation coarser (putting
equivalence classes together). And, be warned that there are subobjects and
quotients which are not formed in this simple way.
The proof just given is sketchy in the handling of equivalence classes of maps,
and, in the construction of the equalizer and coequalizer, it has to be checked
that the structures suggested have the required universal properties. But, this
argument-modulo equivalence classes-is exactly similar to what is done for
the catgory Top 0 . We remark that the category of equivalence relations on
sets is included here: a set is just a discrete topological space (and these form
a full subcategory of Top 0
Of course, with the aid of the Axiom of Choice, it
is quickly shown that the category of equivalence relations is equivalent to the
category of sets (via the obvious use of quotient sets). However, the category
Equ introduced here is not equivalent to the category Top 0 . For one thing,
no topology is being put on the quotient space jEj=j E . And this category has
a property-cartesian closure-that Top 0 does not share.
To investigate Equ further, we introduce a closely connected category.
Definition 3.11 The category PEqu of partial equilogical spaces is defined
as follows.
(1) Objects are structures
hjAj;\Omega A i is the \Sigma-
topology of an algebraic lattice, and where jA is a partial equivalence
relation, i.e., reflexive only on a subset of jAj.
(2) The mappings between partial equilogical spaces are the equivalence
classes of continuous mappings between the algebraic lattices that preserve
the partial equivalence relation, where the equivalence relation on
mappings is defined as before by
These mappings will also be called equivariant.
If we consider the relation f jA!B g as being defined between arbitrary
continuous functions, then equivariant maps for the category PEqu are the
(equivalence classes of) the functions f satisfying f jA!B f , since that means
that the function preserves the underlying equivalence relation. This remark
gives a hint as to how we will define function spaces, but first we want to check
the equivalence of categories.
Theorem 3.12 The categories Equ and PEqu are equivalent.
Proof. The naturally suggested functor from PEqu to Equ is the one that
takes
restricts the topology to the subspace on the subset
g. On this subset the equivalence relation is "total". The
mappings are likewise restricted. Call the functor R (for "restriction"). Now,
a map of PEqu, then
valid as a map of Equ, and identities and compositions are preserved.
We note first that the functor R is faithful by definition. Then, the functor R is
full in view of The Extension Theorem (because continuous functions between
-spaces can be extended to any algebraic lattices embedding them). Finally,
the functor R is essentially surjective on objects by virtue of The Embedding
Theorem (and note that the equivalence relation on the T 0 -space does not
have to be extended but remains partial). This is enough to show that the
categories are equivalent.
The idea of partial equivalence relations has been very widely employed. Scott
believes he first called general attention to it in the late '60s after extracting
it from the studies by G. Kreisel and A. Troelstra on extensional theories
of higher-type functionals in recursion theory. However, it has been mostly
used recently in the context of giving types to (quotients of) subsets of a
universal model of some sort. We think allowing partial equivalence relations
over a large category (such as algebraic lattices) is possibly a new idea; but,
certainly, many familiar proofs get reused in the new context. The following
theorem is an example of this reuse.
Theorem 3.13 The category Equ is cartesian closed.
Proof. In view of the previous theorem, we will show that PEqu is cartesian
closed. Given structures A and B in PEqu we define the structure A ! B so
that
is the set of continuous functions between the lattices jAj and
(ii)\Omega A!B is the \Sigma-topology on this algebraic lattice;
(iii) jA!B is the partial equivalence defined previously.
We have to show, that for any three structures in PEqu, say, A, B, and C,
there is a one-one correspondence between functions in in the two spaces:
As we know, there is a particular one-one correspondence that is an isomorphism
of the underlying algebraic lattices (and a homeomorphism of topological
spaces). It only remains to show that the isomorphism preserves the
equivalence relation on the compound space. This is a "self-proving"
theorem, in the sense that once the question is stated it is just a matter of
unpacking the definitions to finish it off.
4 Equilogical Spaces, Type Theory and Logic
We have now already seen that the category of equilogical spaces provides a
model of the simply-typed -calculus, inasmuch as Equ is cartesian closed. In
this section we show that Equ in fact supports a much more expressive type
theory and logic, which can be introduced by using the method of assemblies.
For simplicity, we sometimes write an object
of PEqu as
with A the algebraic lattice
hjAj;\Omega A i and jA the partial equivalence
relation jA . We then write jAj for the underlying set of the algebraic lattice
A.
Modest Sets and Assemblies. We first introduce yet another equivalent
definition of the category Equ, which will allow us to proceed by analogy to
the category of partial equivalence relations over a PCA (see, e.g., [25,1,2]).
Definition 4.1 The category Assm(ALat) of assemblies over the category
of algebraic lattices is defined as follows.
(1) Objects are triples (X; A; E) with X 2 Set, A 2 ALat, and the mapping
in Set is such that E(x) is non-empty for all x 2 X. We
call the elements in E(x) realizers for x.
(2) The morphisms from an object (X; A; E) to an object (X are
functions in Set for which there exists a continuous function
in ALat such that
We call such a function g a realizer for f , and say that tracks f .
Definition 4.2 An object (X; A; E) of Assm(ALat) is called modest iff
x
The full subcatory of Assm(ALat) formed by the modest objects is referred
to as the category of modest sets over algebraic lattices is denoted
Mod(ALat).
Rougly speaking a modest set is an assembly where a realizer a 2 E(x) carries
enough information to determine the element x 2 X uniquely. An example of
an assembly which is not isomorphic to any modest set is (f0; 1g; P f0g; E),
f0g. Here, the realizers tell us nothing at all about
the differences between 0 and 1. term such as "separated" might have
been more descriptive than "modest" - but see the further comments on
terminology below.)
Readers familiar with categories of realizability models based on PCAs will
immediately note the similarity of the above definitions to the well-known
definitions of the categories of modest sets and assemblies over a PCA (see,
e.g., [15,7,24,22]). Those categories both embed into the so-called realizability
topos over the PCA [15]. We do not get a corresponding embedding into a
topos, however; we shall discuss why below.
One useful intuition is to think of the category of algebraic lattices as providing
a typed universe of realizers (cf. the untyped universe of realizers provided by
a PCA). Indeed for many conclusions we do not use any properties of algebraic
lattices beyond the fact that it is a cartesian closed category. For example, we
might use the cartesian closed category @ 0 ALat of countably based algebraic
lattices, equivalent to the category of algebraic sublattices of PN. In this case,
modest sets are really modest in the sense of having their cardinality bounded
by 2 @ 0 . It turns out also that one can obtain more general results based on
only a weakly cartesian closed category of realizers [6]; we shall not go into
that here, preferring for concreteness to stay with the example of all algebraic
lattices.
Theorem 4.3 The categories Equ, PEqu, and Mod(ALat) are all equivalent

Proof. Define a
where a jA a 0 () 9x 2 X:a; a 0 2 E(x). When applied to a morphism
the functor F gives the equivalence
class of a realizer in ALat) for f which exists by virtue
of f being a morphism in Mod(ALat). The definition of F is clearly independent
of the choice of g. It is straightforward to verify that the functor F is
full and faithful and essentially surjective on objects. For the latter, given an
object consider the object (f a 2 jAj j a jA a g=jA ; A; E) 2
Mod(ALat) with E the identity function on equivalence classes.
We now use the alternative description of Equ provided by the above theorem
to present some of its categorical properties in an hopefully illuminating way.
Some of the properties we have already seen, but the the alternative descriptions
below are useful. Along the way, we consider Assm(ALat), since the
constructions are basically the same and we shall make use of Assm(ALat)
below.
First, let us denote that inclusion functor from Mod(ALat) to Assm(ALat)
by I. We now check some categorical properties directly.
Theorem 4.4 Both Assm(ALat) and Mod(ALat) are cartesian closed and
the inclusion preserves the cartesian closed structure:
Proof. The terminal object of Assm(ALat) is (1
g. Clearly it is modest and terminal in
Mod(ALat).
The binary product of (X; A; EX ) and (Y; B;E Y ) is (X \Theta Y; A \Theta B;E) with
Here we make use of the binary products in the
category of algebraic lattices, in analogy with the way in which the product
operation of a PCA is used to prove that the category of assemblies and
modest sets over such has binary products. If (X; A; EX ) and (Y; B;E Y ) are
both modest, then also their product so defined is modest.
The exponential of (X; E) with
E(f) the set of elements of B A which track f ,
g. If (X; A; EX )
and (Y; B;E Y ) are both modest, then also (Z; B A ; E) is modest.
Theorem 4.5 Both Assm(ALat) and Mod(ALat) have finite limits and
the inclusion preserves the finite limits.
Proof. By the previous theorem it suffices to consider equalizers. The equalizer
of f;
X is EX restricted to the subset, together with the obvious inclusion
map. Let us also write out the pullback of f and g in
The object P is (f (x;
(or in Mod(ALat)) exactly if f is an injective function of sets; it is an epimorphism
exactly if f is a surjective function. Let us now consider regular
subobjects.
Recall that a regular category is a category with finite limits and (stable under
image factorizations.
Theorem 4.6 Both Assm(ALat) and Mod(ALat) are regular categories.
Proof. By the previous theorems, it suffices to show that we have stable
image factorizations. The image factorization of f : (X; A; EX
is
e
where
For the mappings, we set (which is tracked by the identity), and
(which is tracked by a realizer for f ).
Theorem 4.7 The regular subobjects of an object (X; A; EX ), both in the category
Assm(ALat) and in Mod(ALat) are in bijective correspondence with
the powerset of X.
Proof. This follows easily from the description of equalizers.
In terms of PEqu, a regular subobject of an object (A; jA ) consists of the
algebraic lattice A together with a partial equivalence relation corresponding
to a collection of the equivalence classes of jA .
The well-known relationship between the category of assemblies over a PCA
and the category of sets (see, e.g., [24]) can easily be generalized to our situation
as well: The category Set of sets embeds into the category of assemblies
by the functor r E) with
trivially realized. Then one
can show that r is full and faithful, preserves finite limits, and coequalizers of
kernel pairs (hence is exact in the sense of Barr [3]) and exponentials. Define
the "global sections"
exact. Moreover, one can easily prove the
following theorem.
Theorem 4.8 The functor \Gamma is left adjoint to r with
The categorical relationship between modest sets and assemblies is given by
this theorem:
Theorem 4.9 The category Mod(ALat) is a reflective subcategory of the
category Assm(ALat).
Proof. The reflection functor R : Assm(ALat) ! Mod(ALat) is defined
as follows. On objects (X; A; E), let R(X; A; E) = (X=-;
x2[x] E(x 0 ). On morphisms f , let R(f) be
the mapping [x] 7! [f(x)].
Modelling Dependent Type Theory. In this subsection we show that
the category Mod(ALat), and thus PEqu, models dependent type theory.
Types are indexed objects of Mod(ALat); the indexing is by objects of
Mod(ALat). The regular subobjects can be used to give us logic to reason
about the types and with respect to which we have full subset types and
full quotient types. See [14,20,22] for more on subset types and quotient types.
The same holds for Assm(ALat), but here, in addition, the logic is higher
order - in short, the point is that the regular subobject classifier is not an
object of Mod(ALat) but it is an object of Assm(ALat); we explain this in
more detail below.
All this works by analogy to the situation for modest sets and assemblies over
a PCA. But the analogy seems to stop here; for example, the modest sets over
a PCA form essentially an internal category in the corresponding category of
assemblies and can be used to give a model of the calculus of constructions
with an impredicative universe of types. We do not have a corresponding result
with modest sets and assemblies over the category of algebraic lattices as we
will explain.
Before embarking on the technical development, let us consider an example.
Let Y be a closed type (an object of Mod(ALat)) and let N denote the
type of natural numbers. Further assume in Mod(ALat). In the
dependent type theory we can then form the type
consisting of all functions, which, given a y produces an n greater or equal to
u(y). Here f n 2 N j n - u(y) g is a well-formed (subset) type in the context
For the technical development, we make use of B. Jacobs' fibrational description
of models of dependent type theory [19,21,22], which is related to the
display-map categories [37,17], categories with attributes [8,27], D-categories [10],
and comprehensive fibrations [29]. See [19] for a comprehensive introduction.
We make a point of describing the models in a so-called "split" way, so as
to avoid problems with interpreting dependent type theory. See, for exam-
ple, [26,31,28,32,13] for a discussion of this issue. As this section progresses,
we assume more and more familiarity with the categories of modest sets, assemblies
and realizability toposes over PCAs. See, for example, [15,18,30] for
background on these categories.
We first define a category of so-called uniform families of objects of the category
Mod(ALat). Uniformity refers to the fact that each object of the family
will have the same underlying algebraic lattice. The idea is that a dependent
type, in a context interpreted by an object I, will be a family of objects
indexed by the object I in Mod(ALat).
Definition 4.10 The category UFam(Mod(ALat)) is defined as follows.
(1) Objects are triples of the form (I; A; (X
(2) Morphisms from an object (I; A; (X
) to an object (J; B; (Y
with
are pairs of the form (f; (f i ) i2X I
for which there exists a ALat such that g tracks f
uniformly, that is,
(3) The identity morphism on an object I = (X I ; A I ; E I ) is (id ; (id) i2X I
(4) The composition of (f; (f i ) i2X I
We think of a family (I; A; (X
a context, with I being the context and (X
being the dependent
type.
Theorem 4.11 The forgetful functor
given by (I; A; (X
is a split fibration which
is equivalent, as a fibration, to the codomain fibration over Mod(ALat).
Proof. Let (J; B; (Y
be an object in the
category UFam(Mod(ALat)) and suppose
Then we can form a family u   (J; B; (Y
I as
). There is then an associated cartesian lifting
(u; (id) i2X I
over u. This choice of liftings forms a splitting.
be the category with objects the morphisms I of
Mod(ALat) and with morphisms from I to
of morphisms in Mod(ALat) such that
Y
I u
commutes. Mod(ALat) be the codomain functor,
a fibration with reindexing given by pullback.
Define the functor P as in
cod
l l l l l l l l l l l l
Mod(ALat)
by mapping an object (I; A; (X
I ), to
I
I \Theta A; E) -
with E(i; (x). The functor P maps a morphism
with to the square
I
I \Theta A; E) fu;fg
I
I u
where fu; fg is the function (i; x) 7! (u(i); f i (x)) tracked by
I \Theta A ! A J \Theta B;
with r u : A I ! A J a realizer for a realizer for the family
. This is, of course, a morphism in ALat since it is defined in the
internal typed lambda calculus language of ALat.
One can now verify that P is a full and faithful fibred functor. Moreover we can
define a fibred functor mapping
to the family
as in
Y
I u
is mapped by Q to (u; (f) i2X I
). It can then be verified that Q is also a fibred
functor and that PQ vertically and that QP vertically.
Consider a type-in-context (I; A; (X
). The functor P, from the proof
above, applied to this type-in-context yields the projection
I
I \Theta A; E) -
I
morphism in Mod(ALat). This projection morphism gives rise to a substitution
functor
I
We think of this functor is as follows. It takes a type in context I and views
it as a type in the extended context ( '
I
I \Theta A; E), corresponding to
the weakening rule
I
The interpretation of I; Type is the functor -   applied to the interpretation
of I To model dependent sums and dependent products,
we need to have left adjoints ' and right adjoints Q to the functor -   .
It is easy to see that (1 Set
) is the terminal object in the
fibre over (using here the same notation
for terminal objects in Set and ALat as before). The terminal object
maps an object I =
to the terminal object over I and a morphism J to the
morphism (u; (-x:  ) i2X I
This terminal object functor has a right adjoint
defined by, for
I
I \Theta A; E) with E(i;
That is, defined in the proof of the previous the-
orem. Briefly, if (u; (f i ) i2X I
) is a morphism from 1(I) to (J; B; (Y
with adjoint transpose from I
to f(J; B; (Y
)g is -i: realized by
where r u is a realizer for r and r f is a relizer for the family (f i ) i2X I
. Thus the
constructions are exactly analoguous to the case for modest sets over a PCA. In
summa, since the terminal object functor has a right adjoint and the projection
functor P is full we have what B. Jacobs calls a split full comprehension
category with unit.
Next, we argue that the compresion category has split products. What this
means is that, for any family
with projection
I
I \Theta A; E) ! I, the reindexing functor
X has a right adjoint Q
X , which satisfies a Beck-Chevalley condition. Define
I
I \Theta A; E); C; (Z
I
to be
where
tracks f" g
It is easy to verify that E 0
i is modest. The adjoint transposes are defined
essentially as for the case of the family of sets fibration; one just has to verify
that one has the requisite realizers, but that is simple using the internal typed
lambda calculus of ALat. Now for the Beck-Chevalley condition, we are to
show that for a pullback
I
I \Theta B;E) fu;idg
I u
in Mod(ALat), we have that the canonical natural transformation
is an identity (not only iso, because we claim to have split products). This is
straightforward to verify.
For the comprehension category to have strong split coproducts (modelling
dependent sums) we need, with notation as in the previous ourparagraph, first
to have left adjoints
X to -
X , for projections -X , satisfying a Beck-Chevalley
condition. Define
I
I \Theta A; E); C; (Z
I
to be
easily seen to be modest. On a morphism
I
X to give (id ; ((x; z) 7! (x; f (i;x) (z))) i2X I
which is clearly realizable. Again it is straightforward to verify that the Beck-
Chevalley condition holds, i.e., referring to the pullback in the previous our-
paragraph, that
Y is an identity. This shows then that we
have split coproducts. To have strong split coproducts, we have to show that
the canonical maps - in
(i;x)2
I
I \Theta A) \Theta C; E
I
I \Theta
I
I \Theta A; E 00
// I
is an isomorphism. But - is just the map ((i; x); z) 7! (i; (x; z)), which is clearly
realizable (by the corresponding map on algebraic lattices!) and clearly has an
inverse. Hence we have strong coproducts.
We have thus shown the following theorem, with notation as in Theorem 4.11
and its proof.
Theorem 4.12 is a split closed
comprehension category. Hence, we have a model of dependent type theory.
We can use the regular subobjects to provide a logic with which one can reason
about the types of the type theory. By Theorem 4.7, the regular subobjects of
an object I = (X I ; A I ; E I ) is isomorphic to PX I . Hence the categoy of regular
subobjects of Mod(ALat), denoted RegSub(Mod(ALat)), can be identified
with the category with objects (I;
and K ' X I and with morphisms from (I; K) to (J; L) maps
Mod(ALat) satisfying that u(K) ' L. In the regular subobject fibration
Mod(ALat)
reindexing of (J; L) along a map given by taking
the inverse image of L along u.
One can use this regular subobject fibration to get a (classical) logic, essentially
as for sets and for regular subobjects of the modest sets over a PCA.
Moreover, with regard to this logic, the comprehension category P admits
full (dependent) subset types and full (dependent) quotient types (see, e.g.,
[20,22,14] for subset types and quotient types). However, for reasons of space,
we do not spell that out here. Instead, let us mention that the above models
of type theory can be also be defined, in the exact same way, for the category
Assm(ALat) of assemblies over algebraic lattices. For this case, the
logic of regular subobjects will be higher-order: the regular subobject fibra-
tion has a generic object, a regular subobject classifier, namely the object
Assm(ALat). Note that this is an object in Assm(ALat) which is not
in Mod(ALat) since it is not modest. Again, this is analogous to the situation
of modest sets and assemblies over a partial combinatory algebra [15,30,22].
Discussion. We should mention that the analogy with categories defined
over a PCA can be made mathematically precise in the sense that there is
a notion of a "weak tripos" - a tripos as in [16] except for the requirement
of a generic object. For such a fibred preorder, one can define a category of
assemblies and modest sets and show that they model dependent type theory.
The tripos for a PCA will then provide an example, as will the weak tripos
constructed over the category of algebraic lattices. The details will appear
elsewhere.
We can also discuss just how far one can consider the analogy with categories
defined over a PCA in an informal way and aimed at the reader already familiar
with the situation for the categories defined over a PCA. We mainly highlight
a couple of interesting questions.
One of the nice features of the modest sets and assemblies over a PCA is
that they can be used to give a model of the calculus construction (see, e.g.,
[18,26,32]). In fact, instead of the category of modest sets one uses the equivalent
category of partial equivalence relations to get a small category. The
crucical point is that this small category can be seen as an internal category
in the category of assemblies and that the externalization of this internal category
is a fibration equivalent to the fibration of uniform modest sets over the
assemblies, which thus has a generic object allowing us to get an impredicative
small universe of types as in the calculus of constructions.
An obvious next question is whether we can get something similar in our case
with modest sets and assemblies over algebraic lattices. It turns out that,
in our case working over algebraic lattices (or indeed any cartesian closed
category), the fibration of uniform modest sets over assemblies is complete,
but we cannot show that it is essentially small. This is not suprising since the
category of algebraic lattices is not small. However, even if we only consider a
small cartesian closed category as our category of realizers, the corresponding
fibration is not small (is not equivalent to the externalization of an internal
category).
The obvious solution to try, by analogy with the situation over a PCA, is
to consider the small category of partial equivalence relations as an internal
category in the category of assemblies (simply by embedding it via r as is
done for the case of PCAs), but then the externalization does not consist
of uniform families: each set in the family will have a different underlying
object of realizers. In fact, we have not been able to show that the fibration
of partial equivalence relations is small and, indeed, we believe that it is not,
unless further assumptions are made about the underlying category of realizers
(besides it being a small cartesian closed category).
Another obvious question to ask, following the analogy with categories over a
PCA, is whether PER(ALat) ' Mod(ALat) and Assm(ALat) embed fully
and faithfully into a big "realizability topos over algebraic lattices" (such as the
exact completion of the regular category Assm(ALat)). The answer is no because
PER(ALat) is not well-powered. For note that it embeds fully, faitfully
by a finite limit preserving functor into the exact completion of Assm(ALat),
and so the latter is also non-well-powered and, hence, not a topos. Again, even
if we take a small cartesian closed category as the universe of realizers, it does
not appear to be enough. To overcome this problem we tried to mimick the
proof of Robinson and Rosolini [33], but it cannot be easily generalized. In
other words, it appears that something more needs to be assumed about the
universe of realizers, and we have to leave that as an open question.
5 Equilogical Spaces and Domains with Totality
Kleene-Kreisel countable functionals of finite type [23] occur in various models
of computation. Ershov [11] placed them in a domain-theoretic setting, and
Berger [4] worked out a general notion of totality for domain theory which
subsumes Ershov's hierarchy of finite types. He also extended this approach to
dependent types in his Habilitationsschrift [5]. We show that Berger's codense
and dense objects in domain theory embed fully and faithfully in PEqu,
from which it follows directly by the previous work of Ershov and Berger
that the Kleene-Kreisel functionals are constructed in PEqu by repeated use
of exponentiation starting from the natural numbers object. We begin this
section with a quick overview of totality as defined by Berger [4]. Please refer
to the original paper for details.
Domains with Totality. For our purposes, a domain is an
algebraic consistently-complete directed-complete partially ordered set with
a least element. We may view domains as topological spaces with their \Sigma-
topologies, just as we did with complete lattices. Let Dom be the category of
domains and continuous functions. Domains can also be considered as topologically
closed non-empty subsets of algebraic lattices. Thus ALat is a full
subcategory of Dom. Additionally Dom is a cartesian closed category (see,
e.g., [36] or [1]), and ALat is a full cartesian closed subcategory of Dom. A
domain becomes an algebraic lattice if a "top" element is added to the poset.
This construction produces a functor which, however, is not a reflection and
it does not preserve the ccc-structure.
The following definitions are taken from Berger [4]. We follow the terminology
of Berger [5] in which the term total has been replaced by the term codense.
subset M ' jDj of a domain D is dense if it is dense in the topological
sense, i.e., the closure of M is jDj. We write x " y when elements
are bounded, and x 6" y when they are unbounded.
A finite subset fx separable if there exist open subsets
We say that . It is easily seen that a finite
set is separable if, and only if, it is unbounded. A family of open sets U is
separating if it separates every separable finite set, i.e., for every separable
' jDj there exist members of U that separate it.
The boolean domain B ? is the flat domain for the boolean values tt and ff .
A partial continuous predicate (pcp) on a domain D is a continuous function
. The function-space domain [D denoted by pcp(D).
With each pcp p we associate two disjoint open sets by inverse images:
A subset P ' jpcp(D)j is separating if the corresponding family
is separating.
Given a set M ' jDj let
set M is codense in D if the family E(M) is separating. An element x 2 jDj
is codense if the singleton fxg is codense in D. Every element of a codense set
is codense, but not every set of codense elements is codense. If M ' jDj is a
codense set then the consistency relation " is an equivalence relation on M .
Thus, a codense set M ' jDj can be viewed as a domain D together with a
partial equivalence relation -M , which is just the relation " restricted to M .
A totality on a domain, in the sense of Berger [4], is a dense and codense
subset of a domain. Note that in the original paper by Berger [4] codense sets
are called total. Here we are using the newer terminology of Berger [5].
Given domains with totality M ' jDj and N ' jEj, it is easily seen that the
set M \Theta N ' jDj \Theta jEj is again a totality on the domain D \Theta E. Similarly, by
the Density Theorem in Berger [4] the set
is a totality on the function-space domain [D ! E]. This idea of totality
generalizes the simple-minded connection between total and partial functions
using flat domains. If A is any set, let A? be the flat domain obtained by
adding a bottom element. Then A iself is a totality on A? , and the total
functions of A ! B in Set correspond to (equivalence classes) of functions in
considered as elements of [A? ! B? ].
Partial Equivalence Relations. Let PER(Dom) be the category formed
just like PEqu except that domains are used instead of algebraic lattices, i.e.,
an object of PER(Dom) is a structure
domain and -D is a partial equivalence relation on jDj. Category PER(Dom)
is cartesian closed, and for D; E 2 PER(Dom) we choose the canonical product
and exponential D \Theta E and D ! E whose underlying domains are the
standard product and exponential in Dom, and the partial equivalence real-
tions are defined by
We say that a partial equivalence relation -D on a domain D is dense when
its domain
dom(-D
is a dense subset of D.
Because every algebraic lattice is a domain, PEqu is a full subcategory of
PER(Dom). The top-adding functor maps an
object D 2 PER(Dom) to the object
;\Omega T (D) i is the algebraic lattice obtained from the underlying
domain of D by attaching a compact top element. Functor T maps a morphism
to the morphism T ([f ]) represented by the map
The top-adding functor is a product-preserving reflection, hence PEqu is an
exponential ideal and a sub-ccc of PER(Dom).
In category Dom it is not the case that every continuous
defined on an arbitrary non-empty subset D 0 ' jDj has a continuous extension
to the whole domain jDj. Because of this fact the category PER(Dom)
has certain undesirable properties. However, it is true that every continuous
map defined on a dense subset has a continuous extension; this is an easy
consequence of the Extension Theorem and the fact that a domain becomes
an algebraic lattice when a top element is added to it. These observations
suggest that we should consider only the dense partial equivalence relations
on domains.
Let DPER(Dom) be the full subcategory of PER(Dom) whose partial
equivalence relations are either dense or empty. We are including the empty
equivalence relation here because the only map from an empty subset always
has a continuous extension. The objects whose partial equivalence relations are
empty are exactly the initial objects of DPER(Dom). We have the following
theorem.
Theorem 5.1 DPER(Dom) and PEqu are equivalent.
Proof. In one direction, the equivalence is established by the top-adding functor
PEqu. In the other direction, the equivalence functor
defined as follows. When
(jAj;\Omega A ; ;)
is an initial object, define A. Otherwise K maps an object A 2 PEqu
to an object K(A) whose underlying domain is the set
which is the topological closure of dom(-A ) in jAj, equipped with the sub-space
topology. The partial equivalence relation for K(A) is just -A restricted
to jK(A)j. The functor K maps a morphism [f to the morphism represented
by the restriction f - jK(A)j . Here we assume that the morphism from
an initial object represented by the constant map f : x 7! ?.
If A is initial, K([f ]) is obviously well defined. When A is not initial, K([f ])
is well defined because continuity of f implies that
It is easily checked that K and T establish an equivalence between PEqu and
DPER(Dom).
We would like to represent domains with totality as equilogical spaces. If
' jDj is codense and dense in D, let hD; -M i be the object of PER(Dom)
whose underlying domain is D and the partial equivalence relation -M is
the relation " on M . This identifies domains with totality as objects of the
category DPER(Dom). The following result shows that the morphisms of
DPER(Dom) are the right ones, because the ccc structure of DPER(Dom)
agrees with the formation of products and function-space objects with totality.
Theorem 5.2 Let M ' jDj, N ' jEj be codense and dense subsets in domains
D and E, respectively. Then in DPER(Dom)
Proof. Here it is understood that the product hD; -M i \Theta hE; -N i and the
exponential hD; -M are the canonical ones for PER(Dom). They
are objects in DPER(Dom) by the Density Theorem in Berger [4]. The first
equality follows from the observation that only if,
Objects X and Y have the same underlying domains, so we only have to show
that the two partial equivalence relations coincide. The partial equivalence
relation on X is
Suppose f -X g. Then f; g 2 hM;Ni and it remains to be shown that f " g.
For every x 2 M , since x " x and f -X g, f(x) " g(x), thus by Lemma 7 in
Berger [4] f and g are inseparable, which is equivalent to them being bounded.
Conversely, suppose f; g 2 hM;Ni and f " g. For every x; y 2 M such that
y, it follows that f(x) " g(y) because f(x) - (f - g)(x - y) and g(y) -
This means that f -X g.
Higher Types. The category PEqu is a full sub-ccc of PER(Dom).
Since DPER(Dom) is a full subcategory of PER(Dom) and is equivalent
to PEqu, it is a full sub-ccc of PER(Dom) as well. Theorem 5.2 states
that for codense and dense subsets M ' jDj and N ' jEj, the exponential
coincides with the object h[D ! E]; - hM;Ni i. We may use
this to show that in PEqu the countable functionals of finite types arise as
iterated function spaces of the natural numbers object. For simplicity we only
concentrate on pure finite types skip the details
of how to extend this to the full hierarchy of finite types generated by ', o, \Theta,
and !.
The natural numbers object in DPER(Dom) is the object
whose underlying domain is the flat domain of natural numbers
and the partial equivalence relation -DN 0
is the restriction of identity to N.
Define the hierarchy DN inductively by
where the arrow is formed in DPER(Dom). By Theorem 5.2, this hierarchy is
contained in DPER(Dom) and corresponds exactly to Ershov's and Berger's
construction of countable functionals of pure finite types. It is well known that
the equivalence classes of DN j correspond naturally to the original Kleene-
Kreisel countable functionals of pure type j, see Berger [4] or Ershov [11].
In PEqu the natural numbers object is
is the algebraic lattice of flat natural numbers
with bottom and top, and -N 0
is the restriction of identity to N. The iterated
function spaces are defined inductively by
The hierarchies DN correspond to each other in
view of the equivalence between DPER(Dom) and PEqu, because they are
both built from the natural numbers object by iterated use of exponentiation,
hence the equivalence classes of N j correspond naturally to the Kleene-Kreisel
countable functionals of pure type j.



--R

Domains and Lambda-Calculi

Exact categories.
Total sets and objects in domain theory.
Continuous Functionals of Dependent and Transitive Types.
Type theory via exact categories.
A categorical approach to realizability and polymorphic types.
Generalized algebraic theories and contextual categories.
Introduction to Lattices and Order.
A categorical semantics of constructions.
Model c for partial continuous functionals.
A Compendium of Continuous Lattices.
On the interpretation of type theory in locally cartesian closed categories.
A simple model for quotient types.
The effective topos.
Tripos theory.
The theory of constructions: categorical semantics and topos theoretical models.
The discrete objects in the effective topos.
Categorical Type Theory.
Quotients in simple type theory.
Comprehension categories and the semantics of type dependency.
Categorical Logic and Type Theory.
Countable functionals.
Realizability Toposes and Language Semantics.
Constructive natural deduction and its '!-set' interpretation.
Computation and Reasoning.
A category theoretic account of program modules.
Metalanguages and applications.
Predicates and Fibrations.
An introduction to fibrations
Categorical logic.
Program Verification in Synthetic Domain Theory.
Colimit completions and the effective topos.
Cartesian closed exact completions.
A new category?
Mathematical Theory of Domains.
Recursive Domains
--TR
Comprehension categories and the semantics of type dependency
Computation and reasoning
Mathematical theory of domains
A Categorical Approach to Realizability and Polymorphic Types
A Simple Model for Quotient Types
On the Interpretation of Type Theory in Locally Cartesian Closed Categories
Continuous Functionals of Dependent Types and Equilogical Spaces
Type Theory via Exact Categories
A General Notion of Realizability
Developing theories of types and computability via realizability
The realizability approach to computable analysis and topology

--CTR
Reinhold Heckmann, A non-topological view of dcpos as convergence spaces, Theoretical Computer Science, v.305 n.1-3, p.159-186, August
Reinhold Heckmann, A Cartesian closed extension of the category of locales, Mathematical Structures in Computer Science, v.16 n.2, p.231-253, April 2006
Ingo Battenfeld , Matthias Schrder , Alex Simpson, A Convenient Category of Domains, Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.69-99, April, 2007
John C. Reynolds, What do types mean?: from intrinsic to extrinsic semantics, Programming methodology, Springer-Verlag New York, Inc., New York, NY,
realizability;domain theory;type theory;logic;topology