Sheaves, Presheaves and Sheafification in the abstract

The existential completion  introduced in [1] and characterized in [2] has been successfully applied to the
study of dialectica [3] and to arithmetic universes in [4].

Here we further extend the range of applications by producing an abstract treatment  of the notion of presheaves of the sheafification adjunction, including the localic one as an instance as well as realizability topos as suitable topos of j-sheaves.

This talk is based on joint work with M.E. Maietti

[1] D. Trotta. The existential completion, Theory and Applications of Categories, 2020
[2] M.E. Maietti and D. Trotta. A characterization of generalized existential completions, Annals of Pure and Applied Logic, 2023
[3] D. Trotta, M. Spadetto, V. De Paiva. Dialectica Principles via Gödel Doctrines, Theoretical Computer Science, 2023
[4] M.E. Maietti and D. Trotta. Quotients, pure existential completions and arithmetic universes, Theory and Applications of Categories, 2024