A structural investigation on formal topology: coreflection of formal covers and exponentiability

Journal of Symbolic Logic 69 (4):967-1005 (2004)
  Copy   BIBTEX

Abstract

We present and study the category of formal topologies and some of its variants. Two main results are proven. The first is that, for any inductively generated formal cover, there exists a formal topology whose cover extends in the minimal way the given one. This result is obtained by enhancing the method for the inductive generation of the cover relation by adding a coinductive generation of the positivity predicate. Categorically, this result can be rephrased by saying that inductively generated formal topologies are coreflective into inductively generated formal covers. The second result is that unary formal covers are exponentiable in the category of inductively generated formal covers and hence, thanks to the coreflection, unary formal topologies are exponentiable in the category of inductively generated formal topologies. From a localic point of view the exponentiability of unary formal topologies means that algebraic dcpos are exponentiable in the category of open locales. But, the coreflection theorem states that open locales are coreflective in locales and hence, as a consequence of well-known impredicative results on exponentiable locales, it allows to prove that locally compact open locales are exponentiable in the category of open locales

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 98,169

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

The problem of the formalization of constructive topology.Silvio Valentini - 2005 - Archive for Mathematical Logic 44 (1):115-129.
Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
Sublocales in Formal Topology.Steven Vickers - 2007 - Journal of Symbolic Logic 72 (2):463 - 482.
Spatiality and classical logic.Milena Stefanova & Silvio Valentini - 2011 - Mathematical Logic Quarterly 57 (4):432-440.
Topological inductive definitions.Giovanni Curi - 2012 - Annals of Pure and Applied Logic 163 (11):1471-1483.
Aspects of general topology in constructive set theory.Peter Aczel - 2006 - Annals of Pure and Applied Logic 137 (1-3):3-29.
Aspects of general topology in constructive set theory.Peter Azcel - 2006 - Annals of Pure and Applied Logic 137 (1-3):3-29.
Compactness in locales and in formal topology.Steven Vickers - 2006 - Annals of Pure and Applied Logic 137 (1-3):413-438.

Analytics

Added to PP
2010-08-24

Downloads
82 (#215,315)

6 months
13 (#210,031)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Compactness in locales and in formal topology.Steven Vickers - 2006 - Annals of Pure and Applied Logic 137 (1-3):413-438.
Constructive version of Boolean algebra.F. Ciraulo, M. E. Maietti & P. Toto - 2013 - Logic Journal of the IGPL 21 (1):44-62.
Objects: A Study in Kantian Formal Epistemology.Giovanni Boniolo & Silvio Valentini - 2012 - Notre Dame Journal of Formal Logic 53 (4):457-478.

View all 8 citations / Add more citations

References found in this work

Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
The problem of the formalization of constructive topology.Silvio Valentini - 2005 - Archive for Mathematical Logic 44 (1):115-129.
Formal spaces and their effective presentations.Inger Sigstam - 1995 - Archive for Mathematical Logic 34 (4):211-246.

Add more references