The localic compact interval is an Escardo-Simpson interval object

Steven Vickers

Research output: Contribution to journalArticlepeer-review

184 Downloads (Pure)

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 languageEnglish
Pages (from-to)614–629
JournalMathematical Logic Quarterly
Volume63
Issue number6
DOIs
Publication statusPublished - 28 Dec 2017

Keywords

  • Constructive
  • analysis
  • localic
  • real

Fingerprint

Dive into the research topics of 'The localic compact interval is an Escardo-Simpson interval object'. Together they form a unique fingerprint.

Cite this