Aspects of Predicative Algebraic Set Theory III: Sheaves

TL;DR

This paper develops a categorical framework for sheaf models of constructive set theories, demonstrating stability of predicative categories with small maps under internal sheaves, advancing algebraic set theory.

Contribution

It introduces a uniform approach to sheaf models in algebraic set theory using predicative categories with small maps, showing their stability under internal sheaves.

Findings

Predicative categories with small maps are stable under internal sheaves.

Framework enables construction of sheaf models for constructive set theories.

Discusses future directions for algebraic set theory and sheaf models.

Abstract

This is the third installment in a series of papers on algebraic set theory. In it, we develop a uniform approach to sheaf models of constructive set theories based on ideas from categorical logic. The key notion is that of a "predicative category with small maps" which axiomatises the idea of a category of classes and class morphisms, together with a selected class of maps whose fibres are sets (in some axiomatic set theory). The main result of the present paper is that such predicative categories with small maps are stable under internal sheaves. We discuss the sheaf models of constructive set theory this leads to, as well as ideas for future work.