Effectful Toposes and Their Lawvere-Tierney Topologies
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2602.23086
curl -X POST /api/v1/records/arxiv/2602.23086/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2602.23086/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'