Locally subcartesian closed categories

Abstract

We introduce locally subcartesian closed categories: categories with pullbacks equipped with a coherent choice of subobjects of pullbacks, such that the resulting affine base-change functors have right adjoints. We develop the basic theory, emphasizing the analogy with locally cartesian closed categories, and justify the terminology by showing that every slice category is monoidal closed with jointly monic projections. We also extend the theory of polynomials, showing that such a category gives rise to a bicategory of polynomials in the sense of Street, biequivalent to a 2-category of subcartesian polynomial functors. We illustrate this theory with the Lawvere quantale as a basic example and the category of nominal sets as a richer one. This work suggests a natural categorical semantics for an extensional dependent affine type theory with bunched contexts and affine implication.