An Algebraic Abstraction of the Localic Sheafification via the Tripos-to-Topos Construction

TL;DR

This paper develops an algebraic framework that unifies the understanding of localic and realizability toposes, connecting sheafification and supercompactification within the tripos-to-topos construction.

Contribution

It introduces an algebraic abstraction that captures the geometric features of localic presheaves and sheafification in the context of the tripos-to-topos construction.

Findings

Provides a unified geometric framework for localic and realizability toposes.

Connects sheafification with supercompactification of locales.

Applicable to a broad class of toposes from tripos constructions.

Abstract

Localic and realizability toposes are two central classes of toposes in categorical logic, both arising through the Hyland-Johnstone-Pitts tripos-to-topos construction. We investigate their shared geometric features by providing an algebraic abstraction of the notions of localic presheaves, sheafification and their connection to supercompactification of a locale via an instance of the Comparison Lemma. This can be applied to a broad class of toposes obtained to the tripos-to-topos constructions, including all those generated from a tripos based on the classical category of ZFC-sets. These results provide a unified geometric framework for understanding localic and realizability toposes.