{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T19:05:54Z","timestamp":1648753554888},"reference-count":29,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":3388,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2004,12]]},"abstract":"Abstract.<\/jats:title>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.<\/jats:p>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.<\/jats:p>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.<\/jats:p>","DOI":"10.2178\/jsl\/1102022209","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T21:48:01Z","timestamp":1109800081000},"page":"967-1005","source":"Crossref","is-referenced-by-count":11,"title":["A structural investigation on formal topology: coreflection of formal covers and exponentiability"],"prefix":"10.1017","volume":"69","author":[{"given":"Maria Emilia","family":"Maietti","sequence":"first","affiliation":[]},{"given":"Silvio","family":"Valentini","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200007374_ref016","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003450"},{"key":"S0022481200007374_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80742-X"},{"key":"S0022481200007374_ref018","volume-title":"Technical Report 42","author":"Palmgren","year":"2002"},{"key":"S0022481200007374_ref024","unstructured":"Sigstam I. , On formal spaces and their effective presentations, Ph.D. thesis , Department of Mathematics, University of Uppsala, 1990."},{"key":"S0022481200007374_ref001","first-page":"1\u2013168","volume-title":"Handbook of logic in computer science","author":"Abramsky","year":"1994"},{"key":"S0022481200007374_ref028","unstructured":"Vickers S. , The double powerlocale and exponentiation: a case study in geometric logic, Draft, 2001."},{"key":"S0022481200007374_ref027","volume-title":"Archive for Mathematical Logic","author":"Valentini","year":"2004"},{"key":"S0022481200007374_ref025","doi-asserted-by":"publisher","DOI":"10.1007\/BF01469380"},{"key":"S0022481200007374_ref003","unstructured":"Coquand T. , Formal Topology with posets, Manuscript. 1996."},{"key":"S0022481200007374_ref029","volume-title":"Una categoria cartesiana chiusa delle topologie formali","author":"Virgili","year":"1990"},{"key":"S0022481200007374_ref019","first-page":"187\u2013204","volume-title":"Mathematical logic and its applications","author":"Sambin","year":"1987"},{"key":"S0022481200007374_ref022","first-page":"221\u2013244","volume-title":"Twenty five years of constructive type theory, Venice 1995","author":"Sambin","year":"1997"},{"key":"S0022481200007374_ref014","article-title":"Exponentiation of Scott formal topologies","volume":"73","author":"Maietti","year":"2003","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"S0022481200007374_ref002","unstructured":"Battilotti G. and Sambin G. , Pretopologies and a uniform presentation of sup-lattice, quantales and frames, Draft, 2001."},{"key":"S0022481200007374_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(03)00052-6"},{"key":"S0022481200007374_ref009","first-page":"264\u2013281","article-title":"Function spaces in the category of locales","volume":"871","author":"Hyland","year":"1981","journal-title":"Lecture Notes in Mathematics"},{"key":"S0022481200007374_ref010","volume-title":"Stone spaces","author":"Johnstone","year":"1982"},{"key":"S0022481200007374_ref015","volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f","year":"1980"},{"key":"S0022481200007374_ref008","unstructured":"Gebellato S. and Sambin G. , Pointfree continuity and convergence, Draft, 2002."},{"key":"S0022481200007374_ref012","first-page":"309","article-title":"An extension of the Galois theory of Grothendieck","volume":"51","author":"Joyal","year":"1984","journal-title":"Memories of the American Mathematical Society"},{"key":"S0022481200007374_ref011","first-page":"84\u2013116","article-title":"Open locales and exponentiation","volume":"30","author":"Johnstone","year":"1984","journal-title":"Contemporary Mathematics"},{"key":"S0022481200007374_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S0022481200007374_ref021","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00704-1"},{"key":"S0022481200007374_ref017","volume-title":"Programming in Martin L\u00f6f's type theory","author":"Nordstr\u00f6m","year":"1990"},{"key":"S0022481200007374_ref026","first-page":"189\u2013219","article-title":"A cartesian closed category in Martin-L\u00f6f's intuitionistic type theory","volume":"290","author":"Valentini","year":"2003","journal-title":"Theoretica Computer Science"},{"key":"S0022481200007374_ref007","first-page":"545\u2013564","article-title":"Topologies on spaces of continuous functions","volume":"26","author":"Escardo","year":"2001","journal-title":"Topology proceedings"},{"key":"S0022481200007374_ref023","first-page":"319\u2013341","article-title":"Constructive Domain Theory as a branch of Intuitionistic Pointfree Topology","volume":"156","author":"Sambin","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"S0022481200007374_ref006","volume-title":"General Topology","author":"Engelking","year":"1977"},{"key":"S0022481200007374_ref005","volume-title":"Geometry of observations: some contributions to (constructive\u2022) point-free topology","author":"Curi","year":"2004"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200007374","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,6]],"date-time":"2019-05-06T19:39:17Z","timestamp":1557171557000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200007374\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,12]]},"references-count":29,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,12]]}},"alternative-id":["S0022481200007374"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1102022209","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,12]]}}}