Effectful Toposes and Their Lawvere-Tierney Topologies

TL;DR

This paper extends effective toposes to effectful toposes, explores Lawvere-Tierney topologies on them, and links these topologies to computational effects and realizability models.

Contribution

It introduces effectful toposes via lifting evidenced frames and characterizes Lawvere-Tierney topologies, connecting realizability with computational effects.

Findings

Lawvere-Tierney topologies correspond to computational oracles in effectful toposes.

The sheaf topos for the double negation topology is isomorphic to the effectful topos with CPS effects.

The work links realizability relativized by oracles to effects through topos theory.

Abstract

This paper introduces effectful toposes as an extension of the effective topos and investigates their structure relative to Lawvere-Tierney topologies. First, we formulate effectful toposes by lifting the evidenced frame, which is a recently proposed model for effectful computation. Next, we define Lawvere-Tierney topologies on effectful toposes and characterize the sheaves on them. In the effective topos, Lawvere-Tierney topologies are known to correspond to computational oracles. Finally, to demonstrate that our result contributes to the connection between realizability relativized by oracles and effects, we show that the sheaf topos for the double negation topology is isomorphic to the effectful topos with the Continuation-Passing-Style effect; these toposes serve as a model of classical realizability.