The localic compact interval is an Escardo-Simpson interval object

Research output: Contribution to journalArticlepeer-review

Colleges, School and Institutes


The locale corresponding to the real interval [-1,1] is an interval object, in the sense of Escardo and Simpson, in the category of locales. The map c: 2^\omega -> [-1,1], mapping a stream s of signs +/-1 to Sum_{i=1}^\infty s_i 2^{-i}, is a proper localic surjection; it is also expressed as a coequalizer. The proofs are valid in any elementary topos with natural numbers object.


Original languageEnglish
Pages (from-to)614–629
JournalMathematical Logic Quarterly
Issue number6
Publication statusPublished - 28 Dec 2017


  • Constructive, analysis, localic, real