The localic compact interval is an Escard\'o-Simpson interval object

TL;DR

This paper demonstrates that the locale of the real interval [-1,1] functions as an interval object within the category of locales, using a specific surjective map from infinite sign streams to the interval.

Contribution

It establishes that the locale of [-1,1] is an interval object in the category of locales, providing a localic perspective on the classical real interval.

Findings

The locale of [-1,1] is an interval object in the category of locales.

The map from infinite sign streams to [-1,1] is a proper localic surjection.

The map is expressed as a coequalizer.

Abstract

The locale corresponding to the real interval [-1,1] is an interval object, in the sense of Escard\'o and Simpson, in the category of locales. The map c from 2^\omega to [-1,1], mapping a stream s of signs +1 or -1 to \Sum_{i=1}^\infty s_i 2^{-i}, is a proper localic surjection; it is also expressed as a coequalizer.