Switch to: References

Add citations

You must login to add citations.
  1. Maximal and Partial Points in Formal Spaces.Erik Palmgren - 2006 - Annals of Pure and Applied Logic 137 (1):291-298.
    The class of points in a set-presented formal topology is a set, if all points are maximal. To prove this constructively a strengthening of the dependent choice principle to infinite well-founded trees is used.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • A Predicative Completion of a Uniform Space.Josef Berger, Hajime Ishihara, Erik Palmgren & Peter Schuster - 2012 - Annals of Pure and Applied Logic 163 (8):975-980.
  • Aspects of General Topology in Constructive Set Theory.Peter Aczel - 2006 - Annals of Pure and Applied Logic 137 (1):3-29.
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  • Locatedness and Overt Sublocales.Bas Spitters - 2010 - Annals of Pure and Applied Logic 162 (1):36-54.
    Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected.Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of a Bishop compact (...)
    Direct download (10 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Exact Approximations to Stone–Čech Compactification.Giovanni Curi - 2007 - Annals of Pure and Applied Logic 146 (2):103-123.
    Given a locale L and any set-indexed family of continuous mappings , fi:L→Li with compact and completely regular co-domain, a compactification η:L→Lγ of L is constructed enjoying the following extension property: for every a unique continuous mapping exists such that . Considered in ordinary set theory, this compactification also enjoys certain convenient weight limitations.Stone–Čech compactification is obtained as a particular case of this construction in those settings in which the class of [0,1]-valued continuous mappings is a set for all L. (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  • The Uniform Boundedness Theorem and a Boundedness Principle.Hajime Ishihara - 2012 - Annals of Pure and Applied Logic 163 (8):1057-1061.
  • Topological Inductive Definitions.Giovanni Curi - 2012 - Annals of Pure and Applied Logic 163 (11):1471-1483.
    In intuitionistic generalized predicative systems as constructive set theory, or constructive type theory, two categories have been proposed to play the role of the category of locales: the category FSp of formal spaces, and its full subcategory FSpi of inductively generated formal spaces. Considered in impredicative systems as the intuitionistic set theory IZF, FSp and FSpi are both equivalent to the category of locales. However, in the mentioned predicative systems, FSp fails to be closed under basic constructions such as that (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  • On the T 1 Axiom and Other Separation Properties in Constructive Point-Free and Point-Set Topology.Peter Aczel & Giovanni Curi - 2010 - Annals of Pure and Applied Logic 161 (4):560-569.
    In this note a T1 formal space is a formal space whose points are closed as subspaces. Any regular formal space is T1. We introduce the more general notion of a formal space, and prove that the class of points of a weakly set-presentable formal space is a set in the constructive set theory CZF. The same also holds in constructive type theory. We then formulate separation properties for constructive topological spaces , strengthening separation properties discussed elsewhere. Finally we relate (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations