Switch to: References

Add citations

You must login to add citations.
  1. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • On the existence of Stone-Čech compactification.Giovanni Curi - 2010 - Journal of Symbolic Logic 75 (4):1137-1146.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • On some peculiar aspects of the constructive theory of point-free spaces.Giovanni Curi - 2010 - Mathematical Logic Quarterly 56 (4):375-387.
    This paper presents several independence results concerning the topos-valid and the intuitionistic predicative theory of locales. In particular, certain consequences of the consistency of a general form of Troelstra's uniformity principle with constructive set theory and type theory are examined.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Constructive strong regularity and the extension property of a compactification.Giovanni Curi - 2023 - Annals of Pure and Applied Logic 174 (1):103154.
    Download  
     
    Export citation  
     
    Bookmark  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   4 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation