2025/11/10 by Maietti, Maria Emilia, Trotta, Davide
Computer Science · #03G30 #18C10 #18C50 #18D30 #Advanced Algebra and Logic #Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · doi:10.48550/arxiv.2511.06945
openalex publication_date 2025/11/10 · openalex created_date 2025/11/12 · openalex updated_date 2026/07/28
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.