$\sigma$-locales in Formal Topology

A $\sigma$-frame is a poset with countable joins and finite meets in whichbinary meets distribute over countable joins. The aim of this paper is to showthat $\sigma$-frames, actually $\sigma$-locales, can be seen as a branch ofFormal Topology, that is, intuitionistic and predicative point-free topology.Every $\sigma$-frame $L$ is the lattice of Lindel\"of elements (those for whicheach of their covers admits a countable subcover) of a formal topology of aspecific kind which, in its turn, is a presentation of the free frame over $L$.We then give a constructive characterization of the smallest (strongly) dense$\sigma$-sublocale of a given $\sigma$-locale, thus providing a"$\sigma$-version" of a Boolean locale. Our development depends on the axiom ofcountable choice