Counterparts of effective-topos local operators in realizability toposes

Let \a0Eff\a0\boldsymbol{\mathsf{Eff}} be the effective topos, and let \a0RT(K2)\a0\mathsf{RT}(\mathcal{K}_2), \a0RT(K2REC,K2)\a0\mathsf{RT}(\mathcal{K}_2^\mathrm{REC},\mathcal{K}_2), and (EffΔ)(\mathsf{Eff}\downarrow\Delta) be the realizability toposes described in the paper. A local operator is a modality on a topos; the conjecture concerns some of the local operators in \a0Eff\a0\mathsf{Eff} considered by Lee and Van Oosten.

Counterpart conjecture. Some of these local operators have counterparts in the toposes

RT(K2),RT(K2REC,K2),(EffΔ).\mathsf{RT}(\mathcal{K}_2),\qquad \mathsf{RT}(\mathcal{K}_2^\mathrm{REC},\mathcal{K}_2),\qquad (\mathsf{Eff}\downarrow\Delta).

Van Oosten had already shown that the original Lifschitz realizability model has a counterpart in \a0RT(K2)\a0\mathsf{RT}(\mathcal{K}_2), and that a related result holds for \a0q\a0\mathbf{q}-realizability. The conjecture proposes analogous counterparts for some of the local operators, but the source does not establish which operators have them or prove the claim.

Sources & referencesView supporting material

Primary source

Michael Rathjen and Andrew Swan, “Lifschitz Realizability as a Topological Construction”, arXiv:1806.10047 (2018).

Progress summary

Never refreshed

Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.

Solutions 0

No solutions have been posted yet.