LOCAL CARTESIAN CLOSURE OF ELEMENTARY QUOTIENT COMPLETIONS

The elementary quotient completion of an elementary doctrine in the sense of Lawvere was introduced in previous work by the first and third authors. It generalizes the exact completion of a category with finite products and weak pullbacks. In this paper, we characterize when an elementary quotient completion is locally cartesian closed in terms of properties of the elementary doctrine which generates it. It generalizes the characterization of locally cartesian closed exact completions given by the third author with Carboni, in the case that the exact completion is performed on a finite product category with weak pullbacks.