Advances in the Unification of Localic and Realizability Toposes

Localic and realizability toposes are two central classes of toposes in categorical logic. The main difference between these two families is that realizability toposes are the main examples of elementary toposes which are not Grothendieck toposes.

In order to investigate their common features, Hyland, Johnstone and Pitts introduced the tripos-to-topos construction in [1], that is a construction producing a topos starting from a suitable kind of Lawvere doctrine called tripos, and showed that both localic and realizability toposes are instances of this construction. This result was the first fundamental step to unify the treatment of these two classes of toposes.

The main purpose of this talk is to carry on this line, by focusing on the geometric properties of localic toposes and on how to generalize them to triposes and toposes obtained from them.

In detail, we show that every topos obtained from a tripos whose base category has weak dependent products and a generic proof is a topos of $j$-sheaves with respect to a suitable Lawvere-Tierney topology over a topos abstracting the sheafification and, respectively, the notion of localic presheaf category [7].

We prove that this topos of abstract presheaves is precisely the topos obtained by applying the $\exists$-completion [8] and then the tripos-to-topos construction to the starting tripos, and that the abstract sheafification arises from a suitable adjunction between the starting tripos and its $\exists$-completion.

Relevant examples include all the toposes obtained from triposes whose base category is $\mathrm{𝖲𝖾𝗍}$, such as: localic toposes, the Effective topos, the Modified Realizability topos [2], the Extensional Realizability topos [3], the Dialectica topos [4], the Krivine topos [5]. As a further significant example of a topos obtained from a tripos that is not $\mathrm{𝖲𝖾𝗍}$-based, we mention the topos of extended Weihrauch degrees recently introduced in [6].

Then we show that the tripos-to-topos and the $\exists$-completion constructions can be combined to produce a tower of toposes, where each topos is a topos of $j$-sheaves for the following one, from a given tripos. The abstract topos of presheaves turns out to be the second step of this tower.

Finally, we show how our analysis is flexible enough to be generalized to the context of predicative toposes to include, e.g. the predicative toposes obtained by Martin-Löf’s type theory or Homotopy Type theory.