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.

翻译：本文引入效应性拓扑斯作为有效拓扑斯的扩展，并研究其相对于劳维尔-蒂尔尼拓扑的结构。首先，我们通过提升证据框架（一种最近提出的效应性计算模型）来构建效应性拓扑斯。接着，我们在效应性拓扑斯上定义劳维尔-蒂尔尼拓扑，并刻画其上的层结构。在有效拓扑斯中，已知劳维尔-蒂尔尼拓扑对应于计算谕示。最后，为证明我们的结果有助于建立由谕示相对化的可实现性与效应之间的联系，我们证明双重否定拓扑的层拓扑斯同构于具有续延传递风格效应的效应性拓扑斯；这些拓扑斯可作为经典可实现性的模型。