Topological inductive definitions. (English) Zbl 1270.03132

The concept of locale is a satisfactory substitute for the notion of topological space in an intuitionistic framework. However, the notion of locale is unsatisfactory in the framework of predicative mathematics. For this reason, the categories FSP of formal spaces and FSP\(_i\) of inductively generated formal spaces have been introduced and studied. These categories are equivalent to the category of locales in an impredicative setting, but both are incomplete in some sense.
The article aims at proposing another category, ImLoc, the category of imaginary locales to circumvent the problems of FSP and FSP\(_i\) in the predicative setting. It turns out that ImLoc contains both FSP and FSP\(_i\) as subcategories, and it is equivalent to the categories of locales in the intuitionistic impredicative framework, thus meeting the initial objective.
In simple terms, ImLoc is the opposite of the category of frame presentations, which are structures given by a preordered set over the base of the intended space together with a generalised covering system. The result is that a frame presentation does not always allow to define a concrete frame meeting its structure, but it always allows to identify a structure of opens that may be realised by a concrete frame. For this reason, ImLoc contains enough objects and continuous functions between them to be complete as a category, thus fixing the problem of FSP, and to represent all the formal spaces of interest, overcoming the difficulties of FSP\(_i\).
The paper concludes presenting a few applications: a point-free version of the Tychonoff embedding theorem, and some set-representation theorems.
This article is of prime interest for every mathematician interested in the categorical description of formal topology in constructive and predicative terms.


03F65 Other constructive mathematics
06D22 Frames, locales
18B30 Categories of topological spaces and continuous mappings (MSC2010)
54B10 Product spaces in general topology
Full Text: DOI


[1] Aczel, P., An introduction to inductive definitions, (), 739-782
[2] Aczel, P., The type theoretic interpretation of constructive set theory: choice principles, (), 1-40
[3] Aczel, P., The type theoretic interpretation of constructive set theory: inductive definitions, (), 17-49
[4] Aczel, P., Aspects of general topology in constructive set theory, Ann. pure appl. logic, 137, 1-3, 3-29, (2006) · Zbl 1077.03035
[5] Aczel, P., Equalisers of frames in constructive set theory, () · Zbl 1256.03053
[6] Aczel, P.; Curi, G., On the \(T_1\) axiom and other separation properties in constructive topology, Ann. pure appl. logic, 161, 560-569, (2010) · Zbl 1223.03050
[7] P. Aczel, M. Rathjen, Notes on Constructive Set Theory, Mittag-Leffler Technical Report No.40, 2000/2001.
[8] Bell, J., Toposes and local set theories, (1988), Oxford University Press · Zbl 0649.18004
[9] Coquand, T., Compact spaces and distributive lattices, J. pure appl. algebra, 184, 1-6, (2003) · Zbl 1034.54005
[10] Coquand, T.; Sambin, G.; Smith, J.; Valentini, S., Inductively generated formal topologies, Ann. pure appl. logic, 124, 1-3, 71-106, (2003) · Zbl 1070.03041
[11] Curi, G., On the collection of points of a formal space, Ann. pure appl. logic, 137, 1-3, 126-146, (2006) · Zbl 1086.03052
[12] Curi, G., Exact approximations to stone-čech compactification, Ann. pure appl. logic, 146, 2-3, 103-123, (2007) · Zbl 1139.03044
[13] Curi, G., On some peculiar aspects of the constructive theory of point-free spaces, Math. log. Q., 56, 4, 375-387, (2010) · Zbl 1200.03043
[14] Curi, G., On the existence of stone-čech compactification, J. symbolic logic, 75, 4, 1137-1146, (2010) · Zbl 1225.03089
[15] Fourman, M.; Grayson, R., (), 107-122
[16] Fourman, M.; Scott, D.S., Sheaves and logic, (), 302-401
[17] C.M. Fox, Point-set and point-free topolology in constructive set theory, Ph.D. thesis, University of Manchester, 2005.
[18] Friedman, H., Set theoretic foundations for constructive analysis, Ann. of math., 2, 105, 1-28, (1977) · Zbl 0353.02014
[19] Gambino, N., Heyting-valued interpretations for constructive set theory, Ann. pure appl. logic, 137, 1-3, 164-188, (2006) · Zbl 1077.03038
[20] Johnstone, P.T., Stone spaces, (1982), Cambridge University Press · Zbl 0499.54001
[21] Johnstone, P.T., Sketches of an elephant. A topos theory compendium. II, () · Zbl 1071.18002
[22] Lubarsky, R.S., CZF and second order arithmetic, Ann. pure appl. logic, 141, 1-2, 29-34, (2006) · Zbl 1094.03038
[23] Lubarsky, R.; Rathjen, M., On the constructive Dedekind reals, Log. anal., 1, 2, 131-152, (2008) · Zbl 1162.03034
[24] MacLane, S.; Moerdijk, I., Sheaves in geometry and logic—A first introduction to topos theory, (1992), Springer
[25] Maietti, M.E., Predicative exponentiation of locally compact formal topologies over inductively generated topologies, (), 202-222 · Zbl 1097.03057
[26] P. Martin-Löf, Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, Napoli, 1984.
[27] Palmgren, E., Quotient spaces and coequalisers in formal topology, J. ucs., 11, 1996-2007, (2005) · Zbl 1124.03038
[28] Palmgren, E., Maximal and partial points in formal spaces, Ann. pure appl. logic, 137, 1-3, 291-298, (2006) · Zbl 1079.03060
[29] Palmgren, E., Predicativity problems in point-free topology, (), 221-231 · Zbl 1102.03058
[30] Sambin, G., Intuitionistic formal spaces—a first communication, (), 187-204
[31] Vermeulen, J.J.C., Some constructive results related to compactness and the (strong) Hausdorff property for locales, (), 401-409 · Zbl 0739.18001
[32] Vermeulen, J.J.C., Proper maps of locales, J. pure appl. algebra, 92, 1, 79-107, (1994) · Zbl 0789.54019
[33] Vickers, S., Some constructive roads to Tychonoff, (), 223-238 · Zbl 1097.03058
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.