A topos for monotone modified realizability using arrow algebras
Zhaorui Hu

Abstract:
We use arrow algebras to construct a topos for monotone modified realizability. We also define a category of assemblies that characterizes the ¬¬-separated objects in the topos. We discuss common logical principles, including independence of premise, the axiom of choice, and the existence of the Fan recursor, in our topos.