Aspects of general topology in constructive set theory

Annals of Pure and Applied Logic 137 (1-3):3-29 (2006)
  Copy   BIBTEX

Abstract

Working in constructive set theory we formulate notions of constructive topological space and set-generated locale so as to get a good constructive general version of the classical Galois adjunction between topological spaces and locales. Our notion of constructive topological space allows for the space to have a class of points that need not be a set. Also our notion of locale allows the locale to have a class of elements that need not be a set. Class sized mathematical structures need to be allowed for in constructive set theory because the powerset axiom and the full separation scheme are necessarily missing from constructive set theory. We also consider the notion of a formal topology, usually treated in Intuitionistic type theory, and show that the category of set-generated locales is equivalent to the category of formal topologies. We exploit ideas of Palmgren and Curi to obtain versions of their results about when the class of formal points of a set-presentable formal topology form a set

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 94,549

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Aspects of general topology in constructive set theory.Peter Azcel - 2006 - Annals of Pure and Applied Logic 137 (1-3):3-29.
Topological inductive definitions.Giovanni Curi - 2012 - Annals of Pure and Applied Logic 163 (11):1471-1483.
Quotient topologies in constructive set theory and type theory.Hajime Ishihara & Erik Palmgren - 2006 - Annals of Pure and Applied Logic 141 (1):257-265.
Locatedness and overt sublocales.Bas Spitters - 2010 - Annals of Pure and Applied Logic 162 (1):36-54.
On the formal points of the formal topology of the binary tree.Silvio Valentini - 2002 - Archive for Mathematical Logic 41 (7):603-618.
Mereology on Topological and Convergence Spaces.Daniel R. Patten - 2013 - Notre Dame Journal of Formal Logic 54 (1):21-31.
Non-deterministic inductive definitions.Benno van den Berg - 2013 - Archive for Mathematical Logic 52 (1-2):113-135.

Analytics

Added to PP
2013-12-31

Downloads
59 (#268,930)

6 months
9 (#455,865)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

On the collection of points of a formal space.Giovanni Curi - 2006 - Annals of Pure and Applied Logic 137 (1-3):126-146.
Maximal and partial points in formal spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1-3):291-298.
Exact approximations to Stone–Čech compactification.Giovanni Curi - 2007 - Annals of Pure and Applied Logic 146 (2):103-123.

View all 23 citations / Add more citations

References found in this work

Constructive set theory.John Myhill - 1975 - Journal of Symbolic Logic 40 (3):347-382.
On the collection of points of a formal space.Giovanni Curi - 2006 - Annals of Pure and Applied Logic 137 (1-3):126-146.
Maximal and partial points in formal spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1-3):291-298.

Add more references