Abstract

The locale corresponding to the real interval [ − 1, 1] is an interval object, in the sense of Escardó and Simpson, in the category of locales. The map, mapping a stream s of signs ±1 to, is a proper localic surjection; it is also expressed as a coequalizer. The proofs are valid in any elementary topos with natural numbers object.