The localic compact interval is an Escardo-Simpson interval object

Steven Vickers

doi:10.1002/malq.201500090

The localic compact interval is an Escardo-Simpson interval object

Steven Vickers

Computer Science

Research output: Contribution to journal › Article › peer-review

225 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 language	English
Pages (from-to)	614–629
Journal	Mathematical Logic Quarterly
Volume	63
Issue number	6
DOIs	https://doi.org/10.1002/malq.201500090
Publication status	Published - 28 Dec 2017

Keywords

Constructive
analysis
localic
real

Access to Document

10.1002/malq.201500090

Vickers_The_localic_compact_interval_Mathematical_Logic_Quarterly_2017
This is the peer reviewed version of the following article: Vickers, S. (2017), The localic compact interval is an Escardó-Simpson interval object. Mathematical Logic Quarterly, 63: 614–629, which has been published in final form at http://dx.doi.org/10.1002/malq.201500090. This article may be used for non-commercial purposes in accordance with Wiley Terms and Conditions for Self-Archiving. Eligibility for repository: Checked on 28/7/2017
Accepted author manuscript, 440 KBLicence: None: All rights reserved

Cite this

@article{05b671de5a77415b91f8d7c888b0f141,

title = "The localic compact interval is an Escardo-Simpson interval object",

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\textasciicircum{}\textbackslash{}omega -> [-1,1], mapping a stream s of signs +/-1 to Sum\_\{i=1\}\textasciicircum{}\textbackslash{}infty s\_i 2\textasciicircum{}\{-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.",

keywords = "Constructive, analysis, localic, real",

author = "Steven Vickers",

year = "2017",

month = dec,

day = "28",

doi = "10.1002/malq.201500090",

language = "English",

volume = "63",

pages = "614–629",

journal = "Mathematical Logic Quarterly",

issn = "0942-5616",

publisher = "Wiley",

number = "6",

}

TY - JOUR

T1 - The localic compact interval is an Escardo-Simpson interval object

AU - Vickers, Steven

PY - 2017/12/28

Y1 - 2017/12/28

N2 - 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.

AB - 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.

KW - Constructive

KW - analysis

KW - localic

KW - real

UR - http://arXiv.org/abs/1506.07995

U2 - 10.1002/malq.201500090

DO - 10.1002/malq.201500090

M3 - Article

SN - 0942-5616

VL - 63

SP - 614

EP - 629

JO - Mathematical Logic Quarterly

JF - Mathematical Logic Quarterly

IS - 6

ER -

The localic compact interval is an Escardo-Simpson interval object

Abstract

Keywords

Access to Document

Fingerprint

Cite this