Topical categories of domains
File(s)DTR97-1.pdf (5.08 MB)
Technical report
Author(s)
Vickers, Steven
Type
Report
Abstract
It is shown how many techniques of categorical domain theory can be expressed in the general context of topical categories (where "topical" means internal in the category Top of Grothendieck toposes with geometric morphisms). The underlying topos machinery is hidden by using a geometric form of constructive mathematics, which enables toposes as "generalized topological spaces" to be treated in a transparently spatial way, and also shows the constructivity of the arguments. The theory of strongly algebraic (SFP) domains is given as a case study in which the topical category is Cartesian closed.
Properties of local toposes and of lifting of toposes (sconing) are summarized, and it is shown that the category of toposes has a fixpoint object in the sense of Crole and Pitts. This is used to show that for a local topos, all endomaps have initial algebras, and this provides a general context in which to describe fixpoint constructions including the solution of domain equations involving constructors of mixed variance. Covariance with respect to embedding-projection pairs or adjunctions arises in a natural way.
The paper also provides a summary of constructive results concerning Kuratowski finite sets, including a novel strong induction principle; and shows that the topical categories of sets, finite sets and decidable sets are not Cartesian closed (unlike the cases of finite decidable sets and strongly algebraic domains).
Properties of local toposes and of lifting of toposes (sconing) are summarized, and it is shown that the category of toposes has a fixpoint object in the sense of Crole and Pitts. This is used to show that for a local topos, all endomaps have initial algebras, and this provides a general context in which to describe fixpoint constructions including the solution of domain equations involving constructors of mixed variance. Covariance with respect to embedding-projection pairs or adjunctions arises in a natural way.
The paper also provides a summary of constructive results concerning Kuratowski finite sets, including a novel strong induction principle; and shows that the topical categories of sets, finite sets and decidable sets are not Cartesian closed (unlike the cases of finite decidable sets and strongly algebraic domains).
Date Issued
1996-12-16
Citation
Departmental Technical Report: 97/1, 1996, pp.1-45
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
45
Journal / Book Title
Departmental Technical Report: 97/1
Copyright Statement
© 1995 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published