Stone bases, alias the constructive content of Stone representation
Sara Negri · 2017
This paper provides a constructive proof of Stone representation theorem for distributive lattices, in the framework of G. Sambin’s formal topologies. In order to formalize the result wholly inside Martin- Löf’s Intuitionistic Type Theory, the notion of Stone base is introduced, and it is proved to be equivalent to that of formal topology in which any cover of a basic open admits a finite subcover. The main theorem states that the category of distributive lattices with apartness is equivalent to the category of Stone bases. Finally the results are related to those of Johnstone and to the classical point-set representation.