Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Effectful Toposes and Their Lawvere-Tierney Topologies

Rinta Yamada

TL;DR

It is shown 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.

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.

Effectful Toposes and Their Lawvere-Tierney Topologies

TL;DR

It is shown 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.

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.
Paper Structure (3 sections, 1 theorem, 7 equations, 1 table)

This paper contains 3 sections, 1 theorem, 7 equations, 1 table.

Table of Contents

  1. Introduction
  2. Effectful Topos
  3. Effective Topos as Effectful Topos

Key Result

proposition thmcounterproposition

$\mathrm{EFT}(\mathord{\mathcal{E\!F}})$ is an elementary topos.

Theorems & Definitions (4)

  • definition thmcounterdefinition: Evidenced Frames cohen_evidenced_2021
  • remark thmcounterremark
  • proposition thmcounterproposition
  • remark thmcounterremark