The localic compact interval is an Escardo-Simpson interval object

Research output: Contribution to journalArticlepeer-review

Colleges, School and Institutes

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.

Details

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

Keywords

  • Constructive, analysis, localic, real