Basic Subtoposes of the Effective Topos

S. Lee; J. van Oosten

doi:10.1016/j.apal.2013.04.001

Basic Subtoposes of the Effective Topos

S. Lee, J. van Oosten

extern

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

Abstract

We study the lattice of local operators in Hyland’s Effective Topos. We show that this lattice is a free completion under internal sups indexed by the natural numbers object, generated by what we call basic local operators. We produce many new local operators and we employ a new concept, sight, in order to analyze these. We show that a local operator identified by A.M. Pitts in his thesis, gives a subtopos with classical arithmetic.

Original language	English
Pages (from-to)	866-883
Number of pages	18
Journal	Annals of Pure and Applied Logic
Volume	164
DOIs	https://doi.org/10.1016/j.apal.2013.04.001
Publication status	Published - 2013

Access to Document

10.1016/j.apal.2013.04.001

Embargoed Document

Subtoposes
Final published version, 313 KB
Embargo ends: 1/01/50

Cite this

@article{9960ff8af005466188582c171d78bb7e,

title = "Basic Subtoposes of the Effective Topos",

abstract = "We study the lattice of local operators in Hyland{\textquoteright}s Effective Topos. We show that this lattice is a free completion under internal sups indexed by the natural numbers object, generated by what we call basic local operators. We produce many new local operators and we employ a new concept, sight, in order to analyze these. We show that a local operator identified by A.M. Pitts in his thesis, gives a subtopos with classical arithmetic.",

author = "S. Lee and {van Oosten}, J.",

year = "2013",

doi = "10.1016/j.apal.2013.04.001",

language = "English",

volume = "164",

pages = "866--883",

journal = "Annals of Pure and Applied Logic",

issn = "0168-0072",

publisher = "Elsevier BV",

}

TY - JOUR

T1 - Basic Subtoposes of the Effective Topos

AU - Lee, S.

AU - van Oosten, J.

PY - 2013

Y1 - 2013

N2 - We study the lattice of local operators in Hyland’s Effective Topos. We show that this lattice is a free completion under internal sups indexed by the natural numbers object, generated by what we call basic local operators. We produce many new local operators and we employ a new concept, sight, in order to analyze these. We show that a local operator identified by A.M. Pitts in his thesis, gives a subtopos with classical arithmetic.

AB - We study the lattice of local operators in Hyland’s Effective Topos. We show that this lattice is a free completion under internal sups indexed by the natural numbers object, generated by what we call basic local operators. We produce many new local operators and we employ a new concept, sight, in order to analyze these. We show that a local operator identified by A.M. Pitts in his thesis, gives a subtopos with classical arithmetic.

U2 - 10.1016/j.apal.2013.04.001

DO - 10.1016/j.apal.2013.04.001

M3 - Article

SN - 0168-0072

VL - 164

SP - 866

EP - 883

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

ER -

Basic Subtoposes of the Effective Topos

Abstract

Access to Document

Embargoed Document

Fingerprint

Cite this