Abstract
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 language | English |
---|---|
Pages (from-to) | 614–629 |
Journal | Mathematical Logic Quarterly |
Volume | 63 |
Issue number | 6 |
DOIs | |
Publication status | Published - 28 Dec 2017 |
Keywords
- Constructive
- analysis
- localic
- real