Basic Subtoposes of the Effective Topos

TL;DR

This paper introduces a new tool called sights to analyze local operators in the Effective Topos, revealing new operators and examining a specific operator that satisfies true arithmetic.

Contribution

It develops the sights methodology to study local operators and demonstrates its effectiveness by analyzing new operators and a particular operator from Pitts' thesis.

Findings

Identified new local operators in the Effective Topos.

Established that a specific operator satisfies true arithmetic.

Demonstrated the utility of sights as a tool for topos analysis.

Abstract

We employ a new tool (sights) to investigate local operators in the Effective Topos. A number of new such local operators is analyzed using this machinery. Moreover, we investigate a local operator defined in the thesis of A. Pitts, and establish that its corresponding subtopos satisfies true arithmetic.