Hostname: page-component-78c5997874-g7gxr Total loading time: 0 Render date: 2024-11-05T04:03:02.515Z Has data issue: false hasContentIssue false
  • English
  • Français

Completeness and cocompleteness of the categories of basic pairs and concrete spaces

Published online by Cambridge University Press:  10 November 2014

HAJIME ISHIHARA  and
TATSUJI KAWAI
HAJIME ISHIHARA
Affiliation:
School of Information Science, Japan Advanced Institute of Science and Technology, 1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan Email: [email protected] and [email protected]
TATSUJI KAWAI
Affiliation:
School of Information Science, Japan Advanced Institute of Science and Technology, 1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan Email: [email protected] and [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We show that the category of basic pairs (BP) and the category of concrete spaces (CSpa) are both small-complete and small-cocomplete in the framework of constructive Zermelo–Frankel set theory extended with the set generation axiom. We also show that CSpa is a coreflective subcategory of BP.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 25 , Special Issue 8: Computing with Infinite Data: Topological and Logical Foundations Part 2 , December 2015 , pp. 1626 - 1648
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aczel, P. (1978) The type theoretic interpretation of constructive set theory. In: MacIntyre, A., Pacholski, L. and Paris, J. (eds.) Logic Colloquium '77, North Holland, Amsterdam 55–66.Google Scholar
Aczel, P. (1982) The type theoretic interpretation of constructive set theory: Choice principles. In: Troelstra, A. S. and van Dalen, D. (eds.) The L.E.J. Brouwer Centenary Symposium, North Holland, Amsterdam 1–40.Google Scholar
Aczel, P. (1986) The type theoretic interpretation of constructive set theory: Inductive definitions. In: Marcus, R. B., Dorn, G. J. and Weingartner, P. (eds.) Logic, Methodology and Philosophy of Science VII, North Holland, Amsterdam 17–49.Google Scholar
Aczel, P. (2006) Aspects of general topology in constructive set theory. Annals of Pure and Applied Logic 137 (13) 3–29.Google Scholar
Aczel, P., Ishihara, H., Nemoto, T. and Sangu, Y. (2014) Generalized geometric theories and set-generated classes. submitted.Google Scholar
Aczel, P. and Rathjen, M. (2000/2001) Notes on constructive set theory. Technical Report 40, Institut Mittag-Leffler, Sweden.Google Scholar
Bishop, E. (1967) Foundations of Constructive Analysis. McGraw-Hill, New York.Google Scholar
Bucalo, A. and Rosolini, G. (2006) Completions, comonoids, and topological spaces. Annals of Pure and Applied Logic 137 (13) 104–125.CrossRefGoogle Scholar
Coquand, T., Sambin, G., Smith, J. and Valentini, S. (2003) Inductively generated formal topologies. Annals of Pure and Applied Logic 124 (13) 71–106.Google Scholar
Fox, C. (2005) Point-Set and Point-Free Topology in Constructive Set Theory, Ph.D. thesis, University of Manchester.Google Scholar
Ishihara, H. and Palmgren, E. (2006) Quotient topologies in constructive set theory and type theory. Annals of Pure and Applied Logic 141 (12) 257–265.CrossRefGoogle Scholar
Ishihara, H. and Schuster, P. (2004) Compactness under constructive scrutiny. Mathematical Logic Quarterly 50 (6) 540–550.Google Scholar
Mac Lane, S. (1998) Categories for the Working Mathematician, 2nd edition, Graduate Texts in Mathematics volume 5, Springer, New York.Google Scholar
Martin-Löf, P. (1984) Intuitionistic type theory, Bibliopolis, Napoli.Google Scholar
Palmgren, E. (2005) Quotient spaces and coequalisers in formal topology. Journal of Universal Computer Science 11 (12) 1996–2007.Google Scholar
Palmgren, E. (2006) Predicativity problems in point-free topology. In: Stoltenberg-Hansen, V. and Väänänen, J. (eds.) Logic Colloquium '03, Lecture Notes in Logic volume 24, Association for Symbolic Logic.Google Scholar
Sambin, G. (1987) Intuitionistic formal spaces – a first communication. In: Skordev, D. (ed.) Mathematical Logic and its Applications, volume 305, Plenum Press 187–204.CrossRefGoogle Scholar
Sambin, G. (to appear) The Basic Picture and Positive Topology. New structures for Constructive Mathematics. Oxford University Press.Google Scholar
Sambin, G. and Gebellato, S. (1999) A preview of the basic picture: A new perspective on formal topology. In: Altenkirch, T., Reus, B. and Naraschewski, W. (eds.) Types for Proofs and Programs. Springer Lecture Notes in Computer Science 1657 194–208.Google Scholar
Spreen, D. (2010) Limits in the basic picture. The presentation given at Workshop on Constructive Topology, Palermo, Italy.Google Scholar