Switch to: Citations

Add references

You must login to add references.
  1. Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
    Formal topology aims at developing general topology in intuitionistic and predicative mathematics. Many classical results of general topology have been already brought into the realm of constructive mathematics by using formal topology and also new light on basic topological notions was gained with this approach which allows distinction which are not expressible in classical topology. Here we give a systematic exposition of one of the main tools in formal topology: inductive generation. In fact, many formal topologies can be presented in (...)
    Download  
     
    Export citation  
     
    Bookmark   44 citations  
  • Compactness in locales and in formal topology.Steven Vickers - 2006 - Annals of Pure and Applied Logic 137 (1-3):413-438.
    If a locale is presented by a “flat site”, it is shown how its frame can be presented by generators and relations as a dcpo. A necessary and sufficient condition is derived for compactness of the locale . Although its derivation uses impredicative constructions, it is also shown predicatively using the inductive generation of formal topologies. A predicative proof of the binary Tychonoff theorem is given, including a characterization of the finite covers of the product by basic opens. The discussion (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations