The associated sheaf functor theorem in algebraic set theory (Q958487)

Algebraic Set Theory has developed as a means of constructing models of nonclassical set theories in a manner analogous to how models of classical set theories are constructed using the method of forcing. To quote the author's summary: ``We prove a version of the associated sheaf functor theorem in Algebraic Set Theory. The proof is established working within a Heyting pretopos equipped with a system of small maps satisfying the axioms originally introduced by Joyal and Moerdijk. This result improves on the existing developments by avoiding the assumption of additional axioms for small maps and the use of collection sites.'' The version referred to above is the following: If \((\mathcal{E},\mathcal{S})\) is a Heyting pretopos equipped with a class of small maps (think of a category of classes in which a notion of smallness singles out the sets), then for every internal Grothendieck site with small covers, the inclusion functor from that site into the category of internal presheaves over that site has a left adjoint which preserves finite limits.