Locally subcartesian closed categories
Charles Walker
Abstract:
We extend the basic theory of locally cartesian closed categories to
the setting in which one has a left adjoint base change given by a
coherent choice of subobjects of pullbacks (subcartesian squares),
where consequently every slice category is symmetric monoidal closed
with jointly monic projections. We justify this extension of the
theory by showing such a category gives rise to a bicategory of
polynomials in the sense of Street, in equivalence with a 2-category
of subcartesian polynomial functors. The interest in these structures
rests on the fact that they should provide a categorical semantics for
dependent affine type theory and underlie the fundamental theorem of
lopos theory. We then show that locally subcartesian categories embed
into closed ones by defining a fibred convolution structure on the
category of presheaves, which we use to find additional examples.